Theorem elab2 3668

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {cab 2702  Vcvv 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802

This theorem is referenced by:  opabidw  5526  opabid  5527  oprabidw  7450  oprabid  7451  soseq  8164  wfrlem3OLDa  8332  tfrlem3a  8398  fsetfcdm  8879  cardprclem  10004  iunfictbso  10139  aceq3lem  10145  dfac5lem4  10151  kmlem9  10183  domtriomlem  10467  ltexprlem3  11063  ltexprlem4  11064  reclem2pr  11073  reclem3pr  11074  supsrlem  11136  supaddc  12214  supadd  12215  supmul1  12216  supmullem1  12217  supmullem2  12218  supmul  12219  01sqrexlem6  15230  infcvgaux2i  15840  mertenslem1  15866  mertenslem2  15867  4sqlem12  16928  conjnmzb  19216  sylow3lem2  19595  mdetunilem9  22566  txuni2  23513  xkoopn  23537  met2ndci  24475  2sqlem8  27404  2sqlem11  27407  madef  27829  eulerpartlemt  34119  eulerpartlemr  34122  eulerpartlemn  34129  subfacp1lem3  34920  subfacp1lem5  34922  rdgssun  36985  finxpsuclem  37004  heiborlem1  37412  heiborlem6  37417  heiborlem8  37419  cllem0  43135  fsetsnf  46568  fsetsnfo  46570  cfsetsnfsetf  46575  cfsetsnfsetf1  46576  cfsetsnfsetfo  46577