Theorem vtoclga 1849

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

Step	Hyp	Ref	Expression
1		ax-17 970	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 970	. 2 |- (ps -> A.xps)
3		vtoclga.1	. 2 |- (x = A -> (ph <-> ps))
4		vtoclga.2	. 2 |- (x e. B -> ph)
5	1, 2, 3, 4	vtoclgaf 1848	1 |- (A e. B -> ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 955   e. wcel 957

This theorem is referenced by:  vtocl2ga 1850  vtocl3ga 1851  vtoclri 1856  ssuni 2518  elinti 2538  ordunisuc 3085  tfis3 3126  fnressn 3832  fressnfv 3833  tfrlem1 3906  tfr2 3920  tz7.44-1 3923  tz7.44-2 3924  tz7.44-3 3925  ndmoprcl 4039  caoprord 4051  caoprmo 4065  erref 4268  erth 4275  elqsi 4284  ecelqsi 4285  supub 4563  suplub 4564  rankr1id 4680  cardcf 4894  subadd 5354  divmul 5684  peano2nn 5893  monoord 6244  om2uzsuc 6246  ser1mono 6287  ser1add2 6288  ser1add 6289  replimt 6707  caure 6879  cauim 6880  ser1absdiflem 6881  fsum1slem 6961  fsump1slem 6965  ser1ser0 7001  serzmulc 7011  serzrelem 7014  climmulc2 7082  serzf0 7122  ser1cmp 7127  ser1cmp2 7130  cvgcmp2lem 7133  cvgcmp3cetlem1 7141  infcvglem3 7175  acdc3 7446  acdc5 7452  cnid 8091  mulid 8096  ringid 8109  minveclem6 8509  minveclem7 8510  minveclem8 8511  hilid 8983  projlem10 9150  cnlnadjlem4 9959  cnlnadjlem5 9960  irredlem3 10275  irredlem4 10276  findreccl 10373

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain