Theorem vtoclga 1852

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 971	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 971	. 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 1851	1 |- (A e. B -> ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958

This theorem is referenced by:  vtocl2ga 1853  vtocl3ga 1854  vtoclri 1859  ssuni 2522  elinti 2542  ordunisuc 3089  tfis3 3130  fnressn 3837  fressnfv 3838  tfrlem1 3911  tfr2 3925  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  ndmoprcl 4044  caoprord 4056  caoprmo 4070  erref 4275  erth 4282  elqsi 4291  ecelqsi 4292  supub 4580  suplub 4581  rankr1id 4697  cardcf 4911  subadd 5371  divmul 5705  peano2nn 5935  monoord 6294  om2uzsuc 6296  ser1mono 6337  ser1add2 6338  ser1add 6339  replimt 6761  caure 6927  cauim 6928  ser1absdiflem 6929  fsum1slem 7008  fsump1slem 7012  ser1ser0 7048  serzmulc 7058  serzrelem 7061  climmulc2 7129  serzf0 7169  ser1cmp 7174  ser1cmp2 7177  cvgcmp2lem 7180  cvgcmp3cetlem1 7188  infcvglem3 7223  acdc3 7487  acdc5 7493  cnid 8127  mulid 8132  ringid 8145  minveclem6 8550  minveclem7 8551  minveclem8 8552  hilid 9028  projlem10 9195  cnlnadjlem4 10003  cnlnadjlem5 10004  irredlem3 10319  irredlem4 10320  findreccl 10417

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain