Theorem abid2 2906

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  {cab 2747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844

This theorem is referenced by:  csbid  3874  csbconstg  3880  csbie  3896  abss  4024  ssab  4025  abssi  4030  notab  4275  dfrab3  4280  notrab  4283  eusn  4701  uniintsn  4954  axrep6g  5255  csbexg  5275  imai  6077  dffv4  6879  orduniss2  7829  dfixp  8897  euen1b  9025  modom2  9212  pwfir  9276  infmap2  10200  ustfn  24328  ustn0  24347  lrrecse  28101  lrrecpred  28103  fpwrelmap  33019  eulerpartlemgvv  34711  ballotlem2  34824  dffv5  36313  ptrest  38158  cnambfre  38207  cnvepresex  38875  pmapglb  40434  polval2N  40570  rngunsnply  43788  iocinico  43831