Theorem elab2 3613

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816

This theorem is referenced by:  elpwOLD  4539  opabidw  5437  opabid  5438  oprabidw  7306  oprabid  7307  wfrlem3OLDa  8142  tfrlem3a  8208  fsetfcdm  8648  cardprclem  9737  iunfictbso  9870  aceq3lem  9876  dfac5lem4  9882  kmlem9  9914  domtriomlem  10198  ltexprlem3  10794  ltexprlem4  10795  reclem2pr  10804  reclem3pr  10805  supsrlem  10867  supaddc  11942  supadd  11943  supmul1  11944  supmullem1  11945  supmullem2  11946  supmul  11947  sqrlem6  14959  infcvgaux2i  15570  mertenslem1  15596  mertenslem2  15597  4sqlem12  16657  conjnmzb  18869  sylow3lem2  19233  mdetunilem9  21769  txuni2  22716  xkoopn  22740  met2ndci  23678  2sqlem8  26574  2sqlem11  26577  eulerpartlemt  32338  eulerpartlemr  32341  eulerpartlemn  32348  subfacp1lem3  33144  subfacp1lem5  33146  soseq  33803  madef  34040  rdgssun  35549  finxpsuclem  35568  heiborlem1  35969  heiborlem6  35974  heiborlem8  35976  cllem0  41173  fsetsnf  44545  fsetsnfo  44547  cfsetsnfsetf  44552  cfsetsnfsetf1  44553  cfsetsnfsetfo  44554