Theorem elab 2950

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	⊢ 𝐴 ∈ V
elab.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elab	⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elab

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
2		elab.1	. 2 ⊢ 𝐴 ∈ V
3		elab.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	elabf 2949	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {cab 2217  Vcvv 2802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804

This theorem is referenced by:  ralab  2966  rexab  2968  intab  3957  dfiin2g  4003  dfiunv2  4006  uniuni  4548  dcextest  4679  peano5  4696  finds  4698  finds2  4699  funcnvuni  5399  fun11iun  5604  elabrex  5898  abrexco  5900  mapval2  6847  ssenen  7037  snexxph  7149  sbthlem2  7157  indpi  7562  nqprm  7762  nqprrnd  7763  nqprdisj  7764  nqprloc  7765  nqprl  7771  nqpru  7772  cauappcvgprlem2  7880  caucvgprlem2  7900  peano1nnnn  8072  peano2nnnn  8073  1nn  9154  peano2nn  9155  dfuzi  9590  hashfacen  11101  shftfvalg  11380  ovshftex  11381  shftfval  11383  4sqlemafi  12970  lss1d  14400  txdis1cn  15005  ushgredgedg  16080  ushgredgedgloop  16082  bj-ssom  16552