Theorem abid2 2636

Description: A simplification of class abstraction. Commuted form of abid1 2635. See comments there. (Contributed by NM, 26-Dec-1993.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		abid1 2635	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2523	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1474   ∈ wcel 1938  {cab 2500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494

This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510

This theorem is referenced by:  csbid  3411  abss  3538  ssab  3539  abssi  3544  notab  3759  dfrab3  3764  notrab  3766  eusn  4112  uniintsn  4347  iunid  4409  csbexg  4619  imai  5288  dffv4  5989  orduniss2  6806  dfixp  7676  euen1b  7793  modom2  7927  infmap2  8803  cshwsexa  13284  ustfn  21722  ustn0  21741  fpwrelmap  28688  eulerpartlemgvv  29576  ballotlem2  29688  dffv5  31040  ptrest  32472  cnambfre  32522  pmapglb  33968  polval2N  34104  rngunsnply  36663  iocinico  36717