Theorem elab2g 2657

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2g.1	|- (x = A -> (ph <-> ps))
elab2g.2	|- B = {x | ph }

Assertion

Ref	Expression
elab2g	|- (A e. V -> (A e. B <-> ps))

Distinct variable groups:   ps,x   x,A

Allowed substitution hints:   ph(x)   B(x)   V(x)

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.2	. . 3 |- B = {x | ph }
2	1	eleq2i 2077	. 2 |- (A e. B <-> A e. {x | ph })
3		elab2g.1	. . 3 |- (x = A -> (ph <-> ps))
4	3	elabg 2656	. 2 |- (A e. V -> (A e. {x | ph } <-> ps))
5	2, 4	syl5bb 181	1 |- (A e. V -> (A e. B <-> ps))

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1223   e. wcel 1366   {cab 1999

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995

This theorem depends on definitions:  df-bi 110  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-v 2528

This theorem is referenced by:  elab2  2658  elab4g  2659  eldif  2895  elun  3052  elin  3094  elprg  3356  elsncg  3361  eluni  3546  eliun  3624  eliin  3625  elopab  3958  elong  4048  opeliunxp  4310  elrn2g  4440  eldmg  4445  elrnmpt  4498  elrnmpt1  4500  elimag  4587  elrnmpt2g  5524  eloprabi  5733  tfrlem3ag  5834  elqsg  6055  1idprl  6415  1idpru  6416  recexprlemell  6443  recexprlemelu  6444