Theorem abid2 2732

Description: A simplification of class abstraction. Commuted form of abid1 2731. 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 2731	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2619	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1475   ∈ wcel 1977  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606

This theorem is referenced by:  csbid  3507  abss  3634  ssab  3635  abssi  3640  notab  3856  dfrab3  3861  notrab  3863  eusn  4209  uniintsn  4449  iunid  4511  csbexg  4720  imai  5397  dffv4  6100  orduniss2  6925  dfixp  7796  euen1b  7913  modom2  8047  infmap2  8923  cshwsexa  13421  ustfn  21815  ustn0  21834  fpwrelmap  28896  eulerpartlemgvv  29765  ballotlem2  29877  dffv5  31201  ptrest  32578  cnambfre  32628  pmapglb  34074  polval2N  34210  rngunsnply  36762  iocinico  36816