Theorem vtoclga 1387

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 group(s):   x,A   x,B   ps,x

Proof of Theorem vtoclga

Step	Hyp	Ref	Expression
1		eleq1 1149	. . . 4 |- (x = A -> (x e. B <-> A e. B))
2		vtoclga.1	. . . 4 |- (x = A -> (ph <-> ps))
3	1, 2	imbi12d 474	. . 3 |- (x = A -> ((x e. B -> ph) <-> (A e. B -> ps)))
4		vtoclga.2	. . 3 |- (x e. B -> ph)
5	3, 4	vtoclg 1383	. 2 |- (A e. B -> (A e. B -> ps))
6	5	pm2.43i 58	1 |- (A e. B -> ps)

Syntax hints:   -> wi 2   <-> wb 127   = wceq 1091   e. wcel 1092

This theorem is referenced by:  vtocl2ga 1388  vtocl3ga 1389  vtoclri 1393  ssuni 1937  elinti 1974  supub 2160  suplub 2161  tfis3 2248  ordunisuc 2339  fnressn 2897  fressnfv 2898  tfrlem1 2949  tfr2 2963  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  ndmoprcl 3058  caoprord 3070  caoprmo 3084  erref 3212  erth 3219  elqsi 3228  ecelqsi 3229  rankr1id 3539  cardcf 3706  subadd 4143  divmul 4218  peano2nn 4433  om2uzsuc 4652  replimt 4798  projlem10 5202

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org