Theorem elab2 3626

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elint  4896  opabidw  5479  opabid  5480  oprabidw  7398  oprabid  7399  soseq  8109  tfrlem3a  8316  fsetfcdm  8807  cardprclem  9903  iunfictbso  10036  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  domtriomlem  10364  ltexprlem3  10961  ltexprlem4  10962  reclem2pr  10971  reclem3pr  10972  supsrlem  11034  supaddc  12123  supadd  12124  supmul1  12125  supmullem1  12126  supmullem2  12127  supmul  12128  01sqrexlem6  15209  infcvgaux2i  15823  mertenslem1  15849  mertenslem2  15850  4sqlem12  16927  conjnmzb  19228  sylow3lem2  19603  mdetunilem9  22585  txuni2  23530  xkoopn  23554  met2ndci  24487  2sqlem8  27389  2sqlem11  27392  madef  27828  eulerpartlemt  34515  eulerpartlemr  34518  eulerpartlemn  34525  subfacp1lem3  35364  subfacp1lem5  35366  dfttc4lem1  36710  dfttc4lem2  36711  rdgssun  37694  finxpsuclem  37713  heiborlem1  38132  heiborlem6  38137  heiborlem8  38139  cllem0  43993  brpermmodel  45430  fsetsnf  47493  fsetsnfo  47495  cfsetsnfsetf  47500  cfsetsnfsetf1  47501  cfsetsnfsetfo  47502