Theorem elab 2751

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 1464	. 2 ⊢ Ⅎ𝑥𝜓
2		elab.1	. 2 ⊢ 𝐴 ∈ V
3		elab.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	elabf 2750	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1287   ∈ wcel 1436  {cab 2071  Vcvv 2615

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617

This theorem is referenced by:  ralab  2766  rexab  2768  intab  3700  dfiin2g  3746  dfiunv2  3749  uniuni  4246  dcextest  4368  peano5  4385  finds  4387  finds2  4388  funcnvuni  5045  fun11iun  5231  elabrex  5492  abrexco  5493  mapval2  6381  ssenen  6513  snexxph  6602  sbthlem2  6604  indpi  6838  nqprm  7038  nqprrnd  7039  nqprdisj  7040  nqprloc  7041  nqprl  7047  nqpru  7048  cauappcvgprlem2  7156  caucvgprlem2  7176  peano1nnnn  7326  peano2nnnn  7327  1nn  8361  peano2nn  8362  dfuzi  8782  hashfacen  10130  shftfvalg  10141  ovshftex  10142  shftfval  10144  bj-ssom  11261