Theorem elab 2986

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 1619	. 2 |- F/xps
2		elab.1	. 2 |- A e. _V
3		elab.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	elabf 2985	1 |- (A e. {x | ph} <-> ps)

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710  {cab 2339  _Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862

This theorem is referenced by:  ralab  2998  rexab  3000  intab  3957  dfiin2g  4001  pwadjoin  4120  dfnnc2  4396  findsd  4411  nnadjoinlem1  4520  tfinnn  4535  vfinncvntsp  4550  vfinspss  4552  vfinspclt  4553  proj1op  4601  proj2op  4602  funcnvuni  5162  fun11iun  5306  tz6.12-2  5347  fnasrn  5418  abrexco  5464  clos1is  5882  mapval2  6019  mucex  6134  ceex  6175  spacis  6289