Theorem elab3 3358

Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)

Hypotheses

Ref	Expression
elab3.1	|- ( ps -> A e. _V )
elab3.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
elab3	|- ( A e. { x | ph } <-> ps )

Distinct variable groups:   ps, x   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem elab3

Step	Hyp	Ref	Expression
1		elab3.1	. 2 |- ( ps -> A e. _V )
2		elab3.2	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	elab3g 3357	. 2 |- ( ( ps -> A e. _V ) -> ( A e. { x | ph } <-> ps ) )
4	1, 3	ax-mp 5	1 |- ( A e. { x | ph } <-> ps )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202

This theorem is referenced by:  fvelrnb  6243  elrnmpt2  6773  ovelrn  6810  isfi  7979  isnum2  8771  pm54.43lem  8825  isfin3  9118  isfin5  9121  isfin6  9122  genpelv  9822  iswrd  13307  4sqlem2  15653  vdwapval  15677  isghm  17660  issrng  18850  lspsnel  19003  lspprel  19094  iscss  20027  ellspd  20141  istps  20738  islp  20944  is2ndc  21249  elpt  21375  itg2l  23496  elply  23951  isismt  25429  isline  35025  ispointN  35028  ispsubsp  35031  ispsubclN  35223  islaut  35369  ispautN  35385  istendo  36048  rngunsnply  37743