Theorem elab2 3199

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1454   e. wcel 1897   {cab 2447   _Vcvv 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058

This theorem is referenced by:  elpw  3968  elint  4253  opabid  4721  elrn2  5092  elimasn  5211  oprabid  6341  wfrlem3a  7063  tfrlem3a  7120  cardprclem  8438  iunfictbso  8570  aceq3lem  8576  dfac5lem4  8582  kmlem9  8613  domtriomlem  8897  ltexprlem3  9488  ltexprlem4  9489  reclem2pr  9498  reclem3pr  9499  supsrlem  9560  supaddc  10601  supadd  10602  supmul1  10603  supmullem1  10604  supmullem2  10605  supmul  10606  sqrlem6  13359  infcvgaux2i  13964  mertenslem1  13988  mertenslem2  13989  4sqlem12  14948  conjnmzb  16965  sylow3lem2  17328  mdetunilem9  19693  txuni2  20628  xkoopn  20652  met2ndci  21585  2sqlem8  24348  2sqlem11  24351  eulerpartlemt  29252  eulerpartlemr  29255  eulerpartlemn  29262  subfacp1lem3  29953  subfacp1lem5  29955  soseq  30540  nofulllem5  30643  finxpsuclem  31833  heiborlem1  32187  heiborlem6  32192  heiborlem8  32194  cllem0  36214