Theorem elab2g 2885

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 2244	. 2 |- ( A e. B <-> A e. { x | ph } )
3		elab2g.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elabg 2884	. 2 |- ( A e. V -> ( A e. { x | ph } <-> ps ) )
5	2, 4	bitrid 192	1 |- ( A e. V -> ( A e. B <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2148   {cab 2163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740

This theorem is referenced by:  elab2  2886  elab4g  2887  eldif  3139  elun  3277  elin  3319  elsng  3608  elprg  3613  eluni  3813  eliun  3891  eliin  3892  elopab  4259  elong  4374  opeliunxp  4682  elrn2g  4818  eldmg  4823  elrnmpt  4877  elrnmpt1  4879  elimag  4975  elrnmpog  5987  eloprabi  6197  tfrlem3ag  6310  tfr1onlem3ag  6338  tfrcllemsucaccv  6355  elqsg  6585  elixp2  6702  isomni  7134  ismkv  7151  iswomni  7163  1idprl  7589  1idpru  7590  recexprlemell  7621  recexprlemelu  7622  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  ismgm  12776  istopg  13502  isbasisg  13547  2sqlem8  14473  2sqlem9  14474