Theorem elab2 3639

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  elint  4916  opabidw  5506  opabid  5507  oprabidw  7447  oprabid  7448  soseq  8160  tfrlem3a  8368  fsetfcdm  8864  cardprclem  9987  iunfictbso  10120  aceq3lem  10126  dfac5lem4  10132  kmlem9  10164  domtriomlem  10447  ltexprlem3  11050  ltexprlem4  11051  reclem2pr  11060  reclem3pr  11061  supsrlem  11123  supaddc  12209  supadd  12210  supmul1  12211  supmullem1  12212  supmullem2  12213  supmul  12214  01sqrexlem6  15336  infcvgaux2i  15949  mertenslem1  15975  mertenslem2  15976  4sqlem12  17052  conjnmzb  19384  sylow3lem2  19759  mdetunilem9  22846  txuni2  23795  xkoopn  23819  met2ndci  24752  2sqlem8  27663  2sqlem11  27666  madef  28102  eulerpartlemt  34884  eulerpartlemr  34887  eulerpartlemn  34894  subfacp1lem3  35763  subfacp1lem5  35765  dfttc4lem1  37149  dfttc4lem2  37150  rdgssun  38134  finxpsuclem  38153  heiborlem1  38563  heiborlem6  38568  heiborlem8  38570  cllem0  44408  brpermmodel  45828  fsetsnf  47941  fsetsnfo  47943  cfsetsnfsetf  47948  cfsetsnfsetf1  47949  cfsetsnfsetfo  47950