Theorem abid2 2361

Description: A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)

Assertion

Ref	Expression
abid2	⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		biid 171	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
2	1	abbi2i 2353	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
3	2	eqcomi 2242	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  {cab 2224

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234

This theorem is used by:  csbid  3155  abss  3317  ssab  3318  abssi  3323  notab  3503  inrab2  3506  dfrab2  3508  dfrab3  3509  notrab  3510  eusn  3785  dfopg  3902  iunid  4068  csbexga  4261  imai  5143  dffv4g  5692  frec0g  6668  dfixp  6982  euen1b  7090  modom2  7109  acfun  7563  ccfunen  7630  ballotfilem2  13228