Theorem elab2g 2911

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 2263	. 2 |- ( A e. B <-> A e. { x | ph } )
3		elab2g.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elabg 2910	. 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 1364   e. wcel 2167   {cab 2182

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765

This theorem is referenced by:  elab2  2912  elab4g  2913  eldif  3166  elun  3304  elin  3346  elsng  3637  elprg  3642  eluni  3842  eliun  3920  eliin  3921  elopab  4292  elong  4408  opeliunxp  4718  elrn2g  4856  eldmg  4861  elrnmpt  4915  elrnmpt1  4917  elimag  5013  elrnmpog  6035  eloprabi  6254  tfrlem3ag  6367  tfr1onlem3ag  6395  tfrcllemsucaccv  6412  elqsg  6644  elixp2  6761  isomni  7202  ismkv  7219  iswomni  7231  1idprl  7657  1idpru  7658  recexprlemell  7689  recexprlemelu  7690  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  4sqexercise1  12567  4sqexercise2  12568  4sqlemsdc  12569  ismgm  13000  istopg  14235  isbasisg  14280  2sqlem8  15364  2sqlem9  15365