Theorem elab 2948

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {cab 2215  Vcvv 2800

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802

This theorem is referenced by:  ralab  2964  rexab  2966  intab  3955  dfiin2g  4001  dfiunv2  4004  uniuni  4546  dcextest  4677  peano5  4694  finds  4696  finds2  4697  funcnvuni  5396  fun11iun  5601  elabrex  5893  abrexco  5895  mapval2  6842  ssenen  7032  snexxph  7143  sbthlem2  7151  indpi  7555  nqprm  7755  nqprrnd  7756  nqprdisj  7757  nqprloc  7758  nqprl  7764  nqpru  7765  cauappcvgprlem2  7873  caucvgprlem2  7893  peano1nnnn  8065  peano2nnnn  8066  1nn  9147  peano2nn  9148  dfuzi  9583  hashfacen  11093  shftfvalg  11372  ovshftex  11373  shftfval  11375  4sqlemafi  12961  lss1d  14390  txdis1cn  14995  ushgredgedg  16070  ushgredgedgloop  16072  bj-ssom  16481