Theorem elab2 3638

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

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

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:  opabidw  5473  opabid  5474  oprabidw  7391  oprabid  7392  soseq  8103  tfrlem3a  8310  fsetfcdm  8801  cardprclem  9895  iunfictbso  10028  aceq3lem  10034  dfac5lem4  10040  dfac5lem4OLD  10042  kmlem9  10073  domtriomlem  10356  ltexprlem3  10953  ltexprlem4  10954  reclem2pr  10963  reclem3pr  10964  supsrlem  11026  supaddc  12113  supadd  12114  supmul1  12115  supmullem1  12116  supmullem2  12117  supmul  12118  01sqrexlem6  15174  infcvgaux2i  15785  mertenslem1  15811  mertenslem2  15812  4sqlem12  16888  conjnmzb  19186  sylow3lem2  19561  mdetunilem9  22568  txuni2  23513  xkoopn  23537  met2ndci  24470  2sqlem8  27397  2sqlem11  27400  madef  27834  eulerpartlemt  34509  eulerpartlemr  34512  eulerpartlemn  34519  subfacp1lem3  35357  subfacp1lem5  35359  rdgssun  37554  finxpsuclem  37573  heiborlem1  37983  heiborlem6  37988  heiborlem8  37990  cllem0  43843  brpermmodel  45280  fsetsnf  47333  fsetsnfo  47335  cfsetsnfsetf  47340  cfsetsnfsetf1  47341  cfsetsnfsetfo  47342