Theorem elab2 3104

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 3103	. 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 1369   e. wcel 1756   {cab 2424   _Vcvv 2967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969

This theorem is referenced by:  elpw  3861  elint  4129  opabid  4591  elrn2  5074  elimasn  5189  oprabid  6110  tfrlem3a  6828  cardprclem  8141  iunfictbso  8276  aceq3lem  8282  dfac5lem4  8288  kmlem9  8319  domtriomlem  8603  ltexprlem3  9199  ltexprlem4  9200  reclem2pr  9209  reclem3pr  9210  supsrlem  9270  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  sqrlem6  12729  infcvgaux2i  13312  mertenslem1  13336  mertenslem2  13337  4sqlem12  14009  conjnmzb  15772  sylow3lem2  16118  mdetunilem9  18401  txuni2  19113  xkoopn  19137  met2ndci  20072  2sqlem8  22686  2sqlem11  22689  eulerpartlemt  26706  eulerpartlemr  26709  eulerpartlemn  26716  subfacp1lem3  27022  subfacp1lem5  27024  soseq  27666  nofulllem5  27798  supaddc  28370  supadd  28371  heiborlem1  28663  heiborlem6  28668  heiborlem8  28670