Theorem elab2 3635

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  elint  4912  opabidw  5497  opabid  5498  oprabidw  7451  oprabid  7452  soseq  8176  tfrlem3a  8385  fsetfcdm  8883  cardprclem  10061  iunfictbso  10194  aceq3lem  10200  dfac5lem4  10206  kmlem9  10238  domtriomlem  10521  ltexprlem3  11124  ltexprlem4  11125  reclem2pr  11134  reclem3pr  11135  supsrlem  11197  supaddc  12285  supadd  12286  supmul1  12287  supmullem1  12288  supmullem2  12289  supmul  12290  01sqrexlem6  15415  infcvgaux2i  16028  mertenslem1  16054  mertenslem2  16055  4sqlem12  17135  conjnmzb  19468  sylow3lem2  19843  mdetunilem9  22936  txuni2  23885  xkoopn  23909  met2ndci  24842  2sqlem8  27754  2sqlem11  27757  madef  28223  eulerpartlemt  35046  eulerpartlemr  35049  eulerpartlemn  35056  acwer1prclem  35808  onprcf1acwevdlem1  35957  subfacp1lem3  36016  subfacp1lem5  36018  dfttc4lem1  37391  dfttc4lem2  37392  rdgssun  38377  finxpsuclem  38396  heiborlem1  38821  heiborlem6  38826  heiborlem8  38828  cllem0  44643  brpermmodel  46069  fsetsnf  48197  fsetsnfo  48199  cfsetsnfsetf  48204  cfsetsnfsetf1  48205  cfsetsnfsetfo  48206