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  27352  eulerpartlemt  33401  eulerpartlemr  33404  eulerpartlemn  33411  subfacp1lem3  34204  subfacp1lem5  34206  rdgssun  36307  finxpsuclem  36326  heiborlem1  36727  heiborlem6  36732  heiborlem8  36734  cllem0  42365  fsetsnf  45809  fsetsnfo  45811  cfsetsnfsetf  45816  cfsetsnfsetf1  45817  cfsetsnfsetfo  45818