Theorem elab 2949

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 2948	1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2201  {cab 2216  Vcvv 2801

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803

This theorem is referenced by:  ralab  2965  rexab  2967  intab  3958  dfiin2g  4004  dfiunv2  4007  uniuni  4550  dcextest  4681  peano5  4698  finds  4700  finds2  4701  funcnvuni  5401  fun11iun  5607  elabrex  5903  abrexco  5905  mapval2  6852  ssenen  7042  snexxph  7154  sbthlem2  7162  indpi  7567  nqprm  7767  nqprrnd  7768  nqprdisj  7769  nqprloc  7770  nqprl  7776  nqpru  7777  cauappcvgprlem2  7885  caucvgprlem2  7905  peano1nnnn  8077  peano2nnnn  8078  1nn  9159  peano2nn  9160  dfuzi  9595  hashfacen  11106  shftfvalg  11401  ovshftex  11402  shftfval  11404  4sqlemafi  12991  lss1d  14421  txdis1cn  15031  ushgredgedg  16106  ushgredgedgloop  16108  bj-ssom  16591