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  3858  dfiin2g  3904  dfiunv2  3907  uniuni  4434  dcextest  4563  peano5  4580  finds  4582  finds2  4583  funcnvuni  5265  fun11iun  5461  elabrex  5734  abrexco  5735  mapval2  6652  ssenen  6825  snexxph  6923  sbthlem2  6931  indpi  7291  nqprm  7491  nqprrnd  7492  nqprdisj  7493  nqprloc  7494  nqprl  7500  nqpru  7501  cauappcvgprlem2  7609  caucvgprlem2  7629  peano1nnnn  7801  peano2nnnn  7802  1nn  8876  peano2nn  8877  dfuzi  9309  hashfacen  10758  shftfvalg  10769  ovshftex  10770  shftfval  10772  txdis1cn  12993  bj-ssom  13893