Theorem elab2 3614

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2109  {cab 2716  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817

This theorem is referenced by:  elpwOLD  4544  opabidw  5439  opabid  5440  oprabidw  7299  oprabid  7300  wfrlem3OLDa  8126  tfrlem3a  8192  fsetfcdm  8622  cardprclem  9721  iunfictbso  9854  aceq3lem  9860  dfac5lem4  9866  kmlem9  9898  domtriomlem  10182  ltexprlem3  10778  ltexprlem4  10779  reclem2pr  10788  reclem3pr  10789  supsrlem  10851  supaddc  11925  supadd  11926  supmul1  11927  supmullem1  11928  supmullem2  11929  supmul  11930  sqrlem6  14940  infcvgaux2i  15551  mertenslem1  15577  mertenslem2  15578  4sqlem12  16638  conjnmzb  18850  sylow3lem2  19214  mdetunilem9  21750  txuni2  22697  xkoopn  22721  met2ndci  23659  2sqlem8  26555  2sqlem11  26558  eulerpartlemt  32317  eulerpartlemr  32320  eulerpartlemn  32327  subfacp1lem3  33123  subfacp1lem5  33125  soseq  33782  madef  34019  rdgssun  35528  finxpsuclem  35547  heiborlem1  35948  heiborlem6  35953  heiborlem8  35955  cllem0  41126  fsetsnf  44496  fsetsnfo  44498  cfsetsnfsetf  44503  cfsetsnfsetf1  44504  cfsetsnfsetfo  44505