Theorem elab 2874

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.)

Hypotheses

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

Assertion

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

Distinct variable groups:   ps, x   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem elab

Step	Hyp	Ref	Expression
1		nfv 1521	. 2 |- F/ x ps
2		elab.1	. 2 |- A e. _V
3		elab.2	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	elabf 2873	1 |- ( A e. { x | ph } <-> ps )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   e. wcel 2141   {cab 2156   _Vcvv 2730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732

This theorem is referenced by:  ralab  2890  rexab  2892  intab  3860  dfiin2g  3906  dfiunv2  3909  uniuni  4436  dcextest  4565  peano5  4582  finds  4584  finds2  4585  funcnvuni  5267  fun11iun  5463  elabrex  5737  abrexco  5738  mapval2  6656  ssenen  6829  snexxph  6927  sbthlem2  6935  indpi  7304  nqprm  7504  nqprrnd  7505  nqprdisj  7506  nqprloc  7507  nqprl  7513  nqpru  7514  cauappcvgprlem2  7622  caucvgprlem2  7642  peano1nnnn  7814  peano2nnnn  7815  1nn  8889  peano2nn  8890  dfuzi  9322  hashfacen  10771  shftfvalg  10782  ovshftex  10783  shftfval  10785  txdis1cn  13072  bj-ssom  13971