Theorem abid2 2874

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  csbid  3851  csbconstg  3857  csbie  3873  abss  4003  ssab  4004  abssi  4009  notab  4255  dfrab3  4260  notrab  4263  eusn  4675  uniintsn  4928  axrep6g  5225  csbexg  5245  imai  6031  dffv4  6829  orduniss2  7775  dfixp  8838  euen1b  8966  modom2  9153  pwfir  9218  infmap2  10128  ustfn  24176  ustn0  24195  lrrecse  27953  lrrecpred  27955  fpwrelmap  32826  eulerpartlemgvv  34541  ballotlem2  34654  dffv5  36125  ptrest  37951  cnambfre  38000  cnvepresex  38668  pmapglb  40227  polval2N  40363  rngunsnply  43612  iocinico  43655