Theorem elab2 3698

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {cab 2717  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  opabidw  5543  opabid  5544  oprabidw  7479  oprabid  7480  soseq  8200  wfrlem3OLDa  8367  tfrlem3a  8433  fsetfcdm  8918  cardprclem  10048  iunfictbso  10183  aceq3lem  10189  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem9  10228  domtriomlem  10511  ltexprlem3  11107  ltexprlem4  11108  reclem2pr  11117  reclem3pr  11118  supsrlem  11180  supaddc  12262  supadd  12263  supmul1  12264  supmullem1  12265  supmullem2  12266  supmul  12267  01sqrexlem6  15296  infcvgaux2i  15906  mertenslem1  15932  mertenslem2  15933  4sqlem12  17003  conjnmzb  19293  sylow3lem2  19670  mdetunilem9  22647  txuni2  23594  xkoopn  23618  met2ndci  24556  2sqlem8  27488  2sqlem11  27491  madef  27913  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemn  34346  subfacp1lem3  35150  subfacp1lem5  35152  rdgssun  37344  finxpsuclem  37363  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  cllem0  43528  fsetsnf  46966  fsetsnfo  46968  cfsetsnfsetf  46973  cfsetsnfsetf1  46974  cfsetsnfsetfo  46975