Theorem elab2 3606

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {cab 2715  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  elpwOLD  4536  opabidw  5431  opabid  5432  oprabidw  7286  oprabid  7287  wfrlem3OLDa  8113  tfrlem3a  8179  fsetfcdm  8606  cardprclem  9668  iunfictbso  9801  aceq3lem  9807  dfac5lem4  9813  kmlem9  9845  domtriomlem  10129  ltexprlem3  10725  ltexprlem4  10726  reclem2pr  10735  reclem3pr  10736  supsrlem  10798  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmullem2  11876  supmul  11877  sqrlem6  14887  infcvgaux2i  15498  mertenslem1  15524  mertenslem2  15525  4sqlem12  16585  conjnmzb  18784  sylow3lem2  19148  mdetunilem9  21677  txuni2  22624  xkoopn  22648  met2ndci  23584  2sqlem8  26479  2sqlem11  26482  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemn  32248  subfacp1lem3  33044  subfacp1lem5  33046  soseq  33730  madef  33967  rdgssun  35476  finxpsuclem  35495  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  cllem0  41062  fsetsnf  44432  fsetsnfo  44434  cfsetsnfsetf  44439  cfsetsnfsetf1  44440  cfsetsnfsetfo  44441