Theorem elab2 3618

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2.1	⊢ 𝐴 ∈ V
elab2.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elab2.3	⊢ 𝐵 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
elab2	⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem elab2

Step	Hyp	Ref	Expression
1		elab2.1	. 2 ⊢ 𝐴 ∈ V
2		elab2.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elab2.3	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
4	2, 3	elab2g 3616	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {cab 2776  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938

This theorem is referenced by:  elpwOLD  4503  opabidw  5377  opabid  5378  elrn2  5785  elimasn  5921  oprabidw  7166  oprabid  7167  wfrlem3a  7940  tfrlem3a  7996  cardprclem  9392  iunfictbso  9525  aceq3lem  9531  dfac5lem4  9537  kmlem9  9569  domtriomlem  9853  ltexprlem3  10449  ltexprlem4  10450  reclem2pr  10459  reclem3pr  10460  supsrlem  10522  supaddc  11595  supadd  11596  supmul1  11597  supmullem1  11598  supmullem2  11599  supmul  11600  sqrlem6  14599  infcvgaux2i  15205  mertenslem1  15232  mertenslem2  15233  4sqlem12  16282  conjnmzb  18385  sylow3lem2  18745  mdetunilem9  21225  txuni2  22170  xkoopn  22194  met2ndci  23129  2sqlem8  26010  2sqlem11  26013  eulerpartlemt  31739  eulerpartlemr  31742  eulerpartlemn  31749  subfacp1lem3  32542  subfacp1lem5  32544  soseq  33209  rdgssun  34795  finxpsuclem  34814  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  cllem0  40265