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 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1402   ∈ wcel 2209  {cab 2224

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234

This theorem is referenced by:  csbid  3155  abss  3317  ssab  3318  abssi  3323  notab  3503  inrab2  3506  dfrab2  3508  dfrab3  3509  notrab  3510  eusn  3781  dfopg  3897  iunid  4063  csbexga  4256  imai  5138  dffv4g  5687  frec0g  6658  dfixp  6972  euen1b  7080  modom2  7099  acfun  7553  ccfunen  7620  ballotfilem2  13206