Theorem elab 2970

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {cab 2224  Vcvv 2821

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823

This theorem is referenced by:  ralab  2986  rexab  2988  intab  3997  dfiin2g  4043  dfiunv2  4046  uniuni  4595  dcextest  4726  peano5  4743  finds  4745  finds2  4746  funcnvuni  5448  fun11iun  5658  elabrex  5957  abrexco  5959  mapfset  6939  mapfoss  6941  fsetsspwxp  6942  mapval2  6953  ssenen  7146  snexxph  7261  sbthlem2  7269  f1setfi  7311  indpi  7703  nqprm  7903  nqprrnd  7904  nqprdisj  7905  nqprloc  7906  nqprl  7912  nqpru  7913  cauappcvgprlem2  8021  caucvgprlem2  8041  peano1nnnn  8213  peano2nnnn  8214  1nn  9298  peano2nn  9299  dfuzi  9739  hashfacen  11267  hashf1lem1  11268  hashf1lem2  11269  shftfvalg  11566  ovshftex  11567  shftfval  11569  4sqlemafi  13157  lss1d  14703  txdis1cn  15362  ushgredgedg  16450  ushgredgedgloop  16452  bj-ssom  16945