Theorem elab2 3098

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 3097	. 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 1362   e. wcel 1755   {cab 2419   _Vcvv 2962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964

This theorem is referenced by:  elpw  3854  elint  4122  opabid  4584  elrn2  5066  elimasn  5182  oprabid  6104  tfrlem3a  6822  cardprclem  8137  iunfictbso  8272  aceq3lem  8278  dfac5lem4  8284  kmlem9  8315  domtriomlem  8599  ltexprlem3  9195  ltexprlem4  9196  reclem2pr  9205  reclem3pr  9206  supsrlem  9266  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  sqrlem6  12721  infcvgaux2i  13303  mertenslem1  13327  mertenslem2  13328  4sqlem12  14000  conjnmzb  15761  sylow3lem2  16107  mdetunilem9  18268  txuni2  18980  xkoopn  19004  met2ndci  19939  2sqlem8  22596  2sqlem11  22599  eulerpartlemt  26602  eulerpartlemr  26605  eulerpartlemn  26612  subfacp1lem3  26918  subfacp1lem5  26920  soseq  27562  nofulllem5  27694  supaddc  28261  supadd  28262  heiborlem1  28554  heiborlem6  28559  heiborlem8  28561