Theorem abid2 2870

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809

This theorem is referenced by:  csbid  3906  csbconstg  3912  csbie  3929  abss  4057  ssab  4058  abssi  4067  notab  4304  dfrab3  4309  notrab  4311  eusn  4734  uniintsn  4991  iunidOLD  5064  axrep6g  5293  csbexg  5310  imai  6073  dffv4  6888  orduniss2  7825  dfixp  8897  euen1b  9031  pwfir  9180  modom2  9249  infmap2  10217  cshwsexaOLD  14780  ustfn  23927  ustn0  23946  lrrecse  27665  lrrecpred  27667  fpwrelmap  32226  eulerpartlemgvv  33674  ballotlem2  33786  dffv5  35201  ptrest  36791  cnambfre  36840  cnvepresex  37507  pmapglb  38945  polval2N  39081  rngunsnply  42218  iocinico  42264