Theorem abid2 2865

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  csbid  3872  csbconstg  3878  csbie  3894  abss  4023  ssab  4024  abssi  4029  notab  4273  dfrab3  4278  notrab  4281  eusn  4690  uniintsn  4945  iunidOLD  5020  axrep6g  5240  csbexg  5260  imai  6034  dffv4  6837  orduniss2  7788  dfixp  8849  euen1b  8976  modom2  9168  pwfir  9242  infmap2  10146  cshwsexaOLD  14766  ustfn  24122  ustn0  24141  lrrecse  27889  lrrecpred  27891  fpwrelmap  32706  eulerpartlemgvv  34360  ballotlem2  34473  dffv5  35905  ptrest  37606  cnambfre  37655  cnvepresex  38311  pmapglb  39757  polval2N  39893  rngunsnply  43151  iocinico  43194