Theorem elab2 3640

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  {cab 2740  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  elint  4917  opabidw  5507  opabid  5508  oprabidw  7443  oprabid  7444  soseq  8153  tfrlem3a  8361  fsetfcdm  8855  cardprclem  9972  iunfictbso  10105  aceq3lem  10111  dfac5lem4  10117  kmlem9  10149  domtriomlem  10432  ltexprlem3  11029  ltexprlem4  11030  reclem2pr  11039  reclem3pr  11040  supsrlem  11102  supaddc  12188  supadd  12189  supmul1  12190  supmullem1  12191  supmullem2  12192  supmul  12193  01sqrexlem6  15305  infcvgaux2i  15919  mertenslem1  15945  mertenslem2  15946  4sqlem12  17022  conjnmzb  19329  sylow3lem2  19704  mdetunilem9  22788  txuni2  23733  xkoopn  23757  met2ndci  24690  2sqlem8  27601  2sqlem11  27604  madef  28040  eulerpartlemt  34770  eulerpartlemr  34773  eulerpartlemn  34780  subfacp1lem3  35682  subfacp1lem5  35684  dfttc4lem1  37067  dfttc4lem2  37068  rdgssun  38052  finxpsuclem  38071  heiborlem1  38490  heiborlem6  38495  heiborlem8  38497  cllem0  44320  brpermmodel  45740  fsetsnf  47816  fsetsnfo  47818  cfsetsnfsetf  47823  cfsetsnfsetf1  47824  cfsetsnfsetfo  47825