Theorem elab2 3649

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  opabidw  5484  opabid  5485  oprabidw  7418  oprabid  7419  soseq  8138  tfrlem3a  8345  fsetfcdm  8833  cardprclem  9932  iunfictbso  10067  aceq3lem  10073  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem9  10112  domtriomlem  10395  ltexprlem3  10991  ltexprlem4  10992  reclem2pr  11001  reclem3pr  11002  supsrlem  11064  supaddc  12150  supadd  12151  supmul1  12152  supmullem1  12153  supmullem2  12154  supmul  12155  01sqrexlem6  15213  infcvgaux2i  15824  mertenslem1  15850  mertenslem2  15851  4sqlem12  16927  conjnmzb  19185  sylow3lem2  19558  mdetunilem9  22507  txuni2  23452  xkoopn  23476  met2ndci  24410  2sqlem8  27337  2sqlem11  27340  madef  27764  eulerpartlemt  34362  eulerpartlemr  34365  eulerpartlemn  34372  subfacp1lem3  35169  subfacp1lem5  35171  rdgssun  37366  finxpsuclem  37385  heiborlem1  37805  heiborlem6  37810  heiborlem8  37812  cllem0  43555  brpermmodel  44993  fsetsnf  47052  fsetsnfo  47054  cfsetsnfsetf  47059  cfsetsnfsetf1  47060  cfsetsnfsetfo  47061