Theorem elab2 3636

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2739  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is used by:  elint  4913  opabidw  5498  opabid  5499  oprabidw  7451  oprabid  7452  soseq  8176  tfrlem3a  8384  fsetfcdm  8882  cardprclem  10060  iunfictbso  10193  aceq3lem  10199  dfac5lem4  10205  kmlem9  10237  domtriomlem  10520  ltexprlem3  11123  ltexprlem4  11124  reclem2pr  11133  reclem3pr  11134  supsrlem  11196  supaddc  12284  supadd  12285  supmul1  12286  supmullem1  12287  supmullem2  12288  supmul  12289  01sqrexlem6  15414  infcvgaux2i  16027  mertenslem1  16053  mertenslem2  16054  4sqlem12  17134  conjnmzb  19467  sylow3lem2  19842  mdetunilem9  22935  txuni2  23884  xkoopn  23908  met2ndci  24841  2sqlem8  27753  2sqlem11  27756  madef  28222  eulerpartlemt  35003  eulerpartlemr  35006  eulerpartlemn  35013  acwer1prclem  35759  onprcf1acwevdlem1  35895  subfacp1lem3  35947  subfacp1lem5  35949  dfttc4lem1  37316  dfttc4lem2  37317  rdgssun  38301  finxpsuclem  38320  heiborlem1  38745  heiborlem6  38750  heiborlem8  38752  cllem0  44566  brpermmodel  45992  fsetsnf  48120  fsetsnfo  48122  cfsetsnfsetf  48127  cfsetsnfsetf1  48128  cfsetsnfsetfo  48129