Theorem elab2 3673

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536   ∈ wcel 2113  {cab 2802  Vcvv 3497

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966

This theorem is referenced by:  elpwOLD  4548  elint  4885  opabidw  5415  opabid  5416  elrn2  5824  elimasn  5957  oprabidw  7190  oprabid  7191  wfrlem3a  7960  tfrlem3a  8016  cardprclem  9411  iunfictbso  9543  aceq3lem  9549  dfac5lem4  9555  kmlem9  9587  domtriomlem  9867  ltexprlem3  10463  ltexprlem4  10464  reclem2pr  10473  reclem3pr  10474  supsrlem  10536  supaddc  11611  supadd  11612  supmul1  11613  supmullem1  11614  supmullem2  11615  supmul  11616  sqrlem6  14610  infcvgaux2i  15216  mertenslem1  15243  mertenslem2  15244  4sqlem12  16295  conjnmzb  18396  sylow3lem2  18756  mdetunilem9  21232  txuni2  22176  xkoopn  22200  met2ndci  23135  2sqlem8  26005  2sqlem11  26008  eulerpartlemt  31633  eulerpartlemr  31636  eulerpartlemn  31643  subfacp1lem3  32433  subfacp1lem5  32435  soseq  33100  rdgssun  34663  finxpsuclem  34682  heiborlem1  35093  heiborlem6  35098  heiborlem8  35100  cllem0  39931