Theorem elab 2896

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2160  {cab 2175  Vcvv 2752

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754

This theorem is referenced by:  ralab  2912  rexab  2914  intab  3891  dfiin2g  3937  dfiunv2  3940  uniuni  4472  dcextest  4601  peano5  4618  finds  4620  finds2  4621  funcnvuni  5307  fun11iun  5504  elabrex  5782  abrexco  5784  mapval2  6708  ssenen  6883  snexxph  6983  sbthlem2  6991  indpi  7376  nqprm  7576  nqprrnd  7577  nqprdisj  7578  nqprloc  7579  nqprl  7585  nqpru  7586  cauappcvgprlem2  7694  caucvgprlem2  7714  peano1nnnn  7886  peano2nnnn  7887  1nn  8965  peano2nn  8966  dfuzi  9398  hashfacen  10857  shftfvalg  10868  ovshftex  10869  shftfval  10871  4sqlemafi  12438  lss1d  13724  txdis1cn  14263  bj-ssom  15174