Theorem elab2 3258

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   {cab 2452   _Vcvv 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120

This theorem is referenced by:  elpw  4022  elint  4294  opabid  4760  elrn2  5248  elimasn  5368  oprabid  6319  tfrlem3a  7058  cardprclem  8372  iunfictbso  8507  aceq3lem  8513  dfac5lem4  8519  kmlem9  8550  domtriomlem  8834  ltexprlem3  9428  ltexprlem4  9429  reclem2pr  9438  reclem3pr  9439  supsrlem  9500  supmul1  10520  supmullem1  10521  supmullem2  10522  supmul  10523  sqrlem6  13061  infcvgaux2i  13649  mertenslem1  13673  mertenslem2  13674  4sqlem12  14350  conjnmzb  16173  sylow3lem2  16521  mdetunilem9  18991  txuni2  19934  xkoopn  19958  met2ndci  20893  2sqlem8  23513  2sqlem11  23516  eulerpartlemt  28135  eulerpartlemr  28138  eulerpartlemn  28145  subfacp1lem3  28451  subfacp1lem5  28453  soseq  29261  nofulllem5  29393  supaddc  29968  supadd  29969  heiborlem1  30234  heiborlem6  30239  heiborlem8  30241  cllem0  37172