Theorem elab2 3681

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {cab 2713  Vcvv 3479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815

This theorem is referenced by:  opabidw  5528  opabid  5529  oprabidw  7463  oprabid  7464  soseq  8185  wfrlem3OLDa  8352  tfrlem3a  8418  fsetfcdm  8901  cardprclem  10020  iunfictbso  10155  aceq3lem  10161  dfac5lem4  10167  dfac5lem4OLD  10169  kmlem9  10200  domtriomlem  10483  ltexprlem3  11079  ltexprlem4  11080  reclem2pr  11089  reclem3pr  11090  supsrlem  11152  supaddc  12236  supadd  12237  supmul1  12238  supmullem1  12239  supmullem2  12240  supmul  12241  01sqrexlem6  15287  infcvgaux2i  15895  mertenslem1  15921  mertenslem2  15922  4sqlem12  16995  conjnmzb  19272  sylow3lem2  19647  mdetunilem9  22627  txuni2  23574  xkoopn  23598  met2ndci  24536  2sqlem8  27471  2sqlem11  27474  madef  27896  eulerpartlemt  34374  eulerpartlemr  34377  eulerpartlemn  34384  subfacp1lem3  35188  subfacp1lem5  35190  rdgssun  37380  finxpsuclem  37399  heiborlem1  37819  heiborlem6  37824  heiborlem8  37826  cllem0  43584  fsetsnf  47068  fsetsnfo  47070  cfsetsnfsetf  47075  cfsetsnfsetf1  47076  cfsetsnfsetfo  47077