Theorem elab 2879

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2146  {cab 2161  Vcvv 2735

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737

This theorem is referenced by:  ralab  2895  rexab  2897  intab  3869  dfiin2g  3915  dfiunv2  3918  uniuni  4445  dcextest  4574  peano5  4591  finds  4593  finds2  4594  funcnvuni  5277  fun11iun  5474  elabrex  5749  abrexco  5750  mapval2  6668  ssenen  6841  snexxph  6939  sbthlem2  6947  indpi  7316  nqprm  7516  nqprrnd  7517  nqprdisj  7518  nqprloc  7519  nqprl  7525  nqpru  7526  cauappcvgprlem2  7634  caucvgprlem2  7654  peano1nnnn  7826  peano2nnnn  7827  1nn  8903  peano2nn  8904  dfuzi  9336  hashfacen  10784  shftfvalg  10795  ovshftex  10796  shftfval  10798  txdis1cn  13358  bj-ssom  14257