HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem vtoclga 1843
Description: Implicit substitution of a class for a set variable.
Hypotheses
Ref Expression
vtoclga.1 |- (x = A -> (ph <-> ps))
vtoclga.2 |- (x e. B -> ph)
Assertion
Ref Expression
vtoclga |- (A e. B -> ps)
Distinct variable groups:   x,A   x,B   ps,x
Proof of Theorem vtoclga
StepHypRef Expression
1 ax-17 968 . 2 |- (y e. A -> A.x y e. A)
2 ax-17 968 . 2 |- (ps -> A.xps)
3 vtoclga.1 . 2 |- (x = A -> (ph <-> ps))
4 vtoclga.2 . 2 |- (x e. B -> ph)
51, 2, 3, 4vtoclgaf 1842 1 |- (A e. B -> ps)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955
This theorem is referenced by:  vtocl2ga 1844  vtocl3ga 1845  vtoclri 1850  ssuni 2512  elinti 2532  ordunisuc 3079  tfis3 3120  fnressn 3822  fressnfv 3823  tfrlem1 3896  tfr2 3910  tz7.44-1 3913  tz7.44-2 3914  tz7.44-3 3915  ndmoprcl 4030  caoprord 4042  caoprmo 4056  erref 4259  erth 4266  elqsi 4275  ecelqsi 4276  supub 4554  suplub 4555  rankr1id 4669  cardcf 4883  subadd 5343  divmul 5674  peano2nn 5883  monoord 6231  om2uzsuc 6233  ser1mono 6274  ser1add2 6275  ser1add 6276  replimt 6692  caure 6864  cauim 6865  ser1absdiflem 6866  fsum1slem 6946  fsump1slem 6950  ser1ser0 6986  serzmulc 6996  serzrelem 6999  climmulc2 7065  serzf0 7105  ser1cmp 7110  ser1cmp2 7113  cvgcmp2lem 7116  cvgcmp3cetlem1 7124  infcvglem3 7158  acdc3 7429  acdc5 7435  cnid 8064  mulid 8069  ringid 8082  minveclem6 8481  minveclem7 8482  minveclem8 8483  hilid 8949  projlem10 9111  cnlnadjlem4 9918  cnlnadjlem5 9919  irredlem3 10227  irredlem4 10228  findreccl 10324
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803
Copyright terms: Public domain