Theorem elab2 3666

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2714  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810

This theorem is referenced by:  opabidw  5504  opabid  5505  oprabidw  7441  oprabid  7442  soseq  8163  wfrlem3OLDa  8330  tfrlem3a  8396  fsetfcdm  8879  cardprclem  9998  iunfictbso  10133  aceq3lem  10139  dfac5lem4  10145  dfac5lem4OLD  10147  kmlem9  10178  domtriomlem  10461  ltexprlem3  11057  ltexprlem4  11058  reclem2pr  11067  reclem3pr  11068  supsrlem  11130  supaddc  12214  supadd  12215  supmul1  12216  supmullem1  12217  supmullem2  12218  supmul  12219  01sqrexlem6  15271  infcvgaux2i  15879  mertenslem1  15905  mertenslem2  15906  4sqlem12  16981  conjnmzb  19241  sylow3lem2  19614  mdetunilem9  22563  txuni2  23508  xkoopn  23532  met2ndci  24466  2sqlem8  27394  2sqlem11  27397  madef  27821  eulerpartlemt  34408  eulerpartlemr  34411  eulerpartlemn  34418  subfacp1lem3  35209  subfacp1lem5  35211  rdgssun  37401  finxpsuclem  37420  heiborlem1  37840  heiborlem6  37845  heiborlem8  37847  cllem0  43565  brpermmodel  45003  fsetsnf  47060  fsetsnfo  47062  cfsetsnfsetf  47067  cfsetsnfsetf1  47068  cfsetsnfsetfo  47069