Theorem elab2 3673

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 3671	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {cab 2710  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811

This theorem is referenced by:  opabidw  5525  opabid  5526  oprabidw  7440  oprabid  7441  soseq  8145  wfrlem3OLDa  8311  tfrlem3a  8377  fsetfcdm  8854  cardprclem  9974  iunfictbso  10109  aceq3lem  10115  dfac5lem4  10121  kmlem9  10153  domtriomlem  10437  ltexprlem3  11033  ltexprlem4  11034  reclem2pr  11043  reclem3pr  11044  supsrlem  11106  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmullem2  12185  supmul  12186  01sqrexlem6  15194  infcvgaux2i  15804  mertenslem1  15830  mertenslem2  15831  4sqlem12  16889  conjnmzb  19127  sylow3lem2  19496  mdetunilem9  22122  txuni2  23069  xkoopn  23093  met2ndci  24031  2sqlem8  26929  2sqlem11  26932  madef  27351  eulerpartlemt  33370  eulerpartlemr  33373  eulerpartlemn  33380  subfacp1lem3  34173  subfacp1lem5  34175  rdgssun  36259  finxpsuclem  36278  heiborlem1  36679  heiborlem6  36684  heiborlem8  36686  cllem0  42317  fsetsnf  45761  fsetsnfo  45763  cfsetsnfsetf  45768  cfsetsnfsetf1  45769  cfsetsnfsetfo  45770