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 1570   ∈ wcel 2145  {cab 2738  Vcvv 3450

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  elint  4912  opabidw  5494  opabid  5495  oprabidw  7439  oprabid  7440  soseq  8154  tfrlem3a  8362  fsetfcdm  8860  cardprclem  10032  iunfictbso  10165  aceq3lem  10171  dfac5lem4  10177  kmlem9  10209  domtriomlem  10492  ltexprlem3  11095  ltexprlem4  11096  reclem2pr  11105  reclem3pr  11106  supsrlem  11168  supaddc  12254  supadd  12255  supmul1  12256  supmullem1  12257  supmullem2  12258  supmul  12259  01sqrexlem6  15382  infcvgaux2i  15995  mertenslem1  16021  mertenslem2  16022  4sqlem12  17096  conjnmzb  19429  sylow3lem2  19804  mdetunilem9  22897  txuni2  23846  xkoopn  23870  met2ndci  24803  2sqlem8  27717  2sqlem11  27720  madef  28156  eulerpartlemt  34938  eulerpartlemr  34941  eulerpartlemn  34948  subfacp1lem3  35868  subfacp1lem5  35870  dfttc4lem1  37238  dfttc4lem2  37239  rdgssun  38221  finxpsuclem  38240  heiborlem1  38665  heiborlem6  38670  heiborlem8  38672  cllem0  44510  brpermmodel  45930  fsetsnf  48043  fsetsnfo  48045  cfsetsnfsetf  48050  cfsetsnfsetf1  48051  cfsetsnfsetfo  48052