Theorem elab2 2954

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 2953	. 2 |- ( A e. _V -> ( A e. B <-> ps ) )
5	1, 4	ax-mp 5	1 |- ( A e. B <-> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   e. wcel 2202   {cab 2217   _Vcvv 2802

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804

This theorem is referenced by:  elpw  3658  elint  3934  opabid  4350  elrn2  4974  elimasn  5103  oprabid  6049  tfrlem3a  6475  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemres  6527  addnqprlemrl  7776  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemrl  7792  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  ltnqpr  7812  ltnqpri  7813  archpr  7862  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemladdfu  7896  caucvgprprlemopu  7918  suplocexprlemloc  7940  4sqlem12  12974  txuni2  14979