Theorem elab 2927

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375   ∈ wcel 2180  {cab 2195  Vcvv 2779

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781

This theorem is referenced by:  ralab  2943  rexab  2945  intab  3931  dfiin2g  3977  dfiunv2  3980  uniuni  4519  dcextest  4650  peano5  4667  finds  4669  finds2  4670  funcnvuni  5366  fun11iun  5569  elabrex  5854  abrexco  5856  mapval2  6795  ssenen  6980  snexxph  7085  sbthlem2  7093  indpi  7497  nqprm  7697  nqprrnd  7698  nqprdisj  7699  nqprloc  7700  nqprl  7706  nqpru  7707  cauappcvgprlem2  7815  caucvgprlem2  7835  peano1nnnn  8007  peano2nnnn  8008  1nn  9089  peano2nn  9090  dfuzi  9525  hashfacen  11025  shftfvalg  11295  ovshftex  11296  shftfval  11298  4sqlemafi  12884  lss1d  14312  txdis1cn  14917  ushgredgedg  15989  ushgredgedgloop  15991  bj-ssom  16209