Theorem elab2 3045

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

Hypotheses

Ref	Expression
elab2.1	|- A e. _V
elab2.2	|- ( x = A -> ( ph <-> ps ) )
elab2.3	|- B = { x | ph }

Assertion

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

Distinct variable groups:   ps, x   x, A

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

Proof of Theorem elab2

Step	Hyp	Ref	Expression
1		elab2.1	. 2 |- A e. _V
2		elab2.2	. . 3 |- ( x = A -> ( ph <-> ps ) )
3		elab2.3	. . 3 |- B = { x | ph }
4	2, 3	elab2g 3044	. 2 |- ( A e. _V -> ( A e. B <-> ps ) )
5	1, 4	ax-mp 8	1 |- ( A e. B <-> ps )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721   {cab 2390   _Vcvv 2916

This theorem is referenced by:  elpw  3765  elint  4016  opabid  4421  elrn2  5068  elimasn  5188  oprabid  6064  cardprclem  7822  iunfictbso  7951  aceq3lem  7957  dfac5lem4  7963  kmlem9  7994  domtriomlem  8278  ltexprlem3  8871  ltexprlem4  8872  reclem2pr  8881  reclem3pr  8882  supsrlem  8942  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  sqrlem6  12008  infcvgaux2i  12592  mertenslem1  12616  mertenslem2  12617  4sqlem12  13279  conjnmzb  14995  sylow3lem2  15217  txuni2  17550  xkoopn  17574  met2ndci  18505  2sqlem8  21109  2sqlem11  21112  subfacp1lem3  24821  subfacp1lem5  24823  soseq  25468  nofulllem5  25574  supaddc  26137  supadd  26138  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918