Theorem elab 2947

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

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

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 2801

This theorem is referenced by:  ralab  2963  rexab  2965  intab  3952  dfiin2g  3998  dfiunv2  4001  uniuni  4542  dcextest  4673  peano5  4690  finds  4692  finds2  4693  funcnvuni  5390  fun11iun  5595  elabrex  5887  abrexco  5889  mapval2  6833  ssenen  7020  snexxph  7125  sbthlem2  7133  indpi  7537  nqprm  7737  nqprrnd  7738  nqprdisj  7739  nqprloc  7740  nqprl  7746  nqpru  7747  cauappcvgprlem2  7855  caucvgprlem2  7875  peano1nnnn  8047  peano2nnnn  8048  1nn  9129  peano2nn  9130  dfuzi  9565  hashfacen  11066  shftfvalg  11337  ovshftex  11338  shftfval  11340  4sqlemafi  12926  lss1d  14355  txdis1cn  14960  ushgredgedg  16032  ushgredgedgloop  16034  bj-ssom  16323