Theorem elab2 3216

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 3215	. 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 1370   e. wcel 1758   {cab 2439   _Vcvv 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080

This theorem is referenced by:  elpw  3977  elint  4245  opabid  4707  elrn2  5190  elimasn  5305  oprabid  6227  tfrlem3a  6949  cardprclem  8264  iunfictbso  8399  aceq3lem  8405  dfac5lem4  8411  kmlem9  8442  domtriomlem  8726  ltexprlem3  9322  ltexprlem4  9323  reclem2pr  9332  reclem3pr  9333  supsrlem  9393  supmul1  10410  supmullem1  10411  supmullem2  10412  supmul  10413  sqrlem6  12859  infcvgaux2i  13442  mertenslem1  13466  mertenslem2  13467  4sqlem12  14139  conjnmzb  15904  sylow3lem2  16252  mdetunilem9  18568  txuni2  19280  xkoopn  19304  met2ndci  20239  2sqlem8  22854  2sqlem11  22857  eulerpartlemt  26921  eulerpartlemr  26924  eulerpartlemn  26931  subfacp1lem3  27237  subfacp1lem5  27239  soseq  27882  nofulllem5  28014  supaddc  28588  supadd  28589  heiborlem1  28881  heiborlem6  28886  heiborlem8  28888