Theorem elab2 3685

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814

This theorem is referenced by:  opabidw  5534  opabid  5535  oprabidw  7462  oprabid  7463  soseq  8183  wfrlem3OLDa  8350  tfrlem3a  8416  fsetfcdm  8899  cardprclem  10017  iunfictbso  10152  aceq3lem  10158  dfac5lem4  10164  dfac5lem4OLD  10166  kmlem9  10197  domtriomlem  10480  ltexprlem3  11076  ltexprlem4  11077  reclem2pr  11086  reclem3pr  11087  supsrlem  11149  supaddc  12233  supadd  12234  supmul1  12235  supmullem1  12236  supmullem2  12237  supmul  12238  01sqrexlem6  15283  infcvgaux2i  15891  mertenslem1  15917  mertenslem2  15918  4sqlem12  16990  conjnmzb  19284  sylow3lem2  19661  mdetunilem9  22642  txuni2  23589  xkoopn  23613  met2ndci  24551  2sqlem8  27485  2sqlem11  27488  madef  27910  eulerpartlemt  34353  eulerpartlemr  34356  eulerpartlemn  34363  subfacp1lem3  35167  subfacp1lem5  35169  rdgssun  37361  finxpsuclem  37380  heiborlem1  37798  heiborlem6  37803  heiborlem8  37805  cllem0  43556  fsetsnf  47001  fsetsnfo  47003  cfsetsnfsetf  47008  cfsetsnfsetf1  47009  cfsetsnfsetfo  47010