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  3864  csbconstg  3870  csbie  3886  abss  4015  ssab  4016  abssi  4021  notab  4265  dfrab3  4270  notrab  4273  eusn  4682  uniintsn  4935  iunidOLD  5010  axrep6g  5229  csbexg  5249  imai  6025  dffv4  6819  orduniss2  7766  dfixp  8826  euen1b  8953  modom2  9141  pwfir  9206  infmap2  10111  cshwsexaOLD  14731  ustfn  24087  ustn0  24106  lrrecse  27854  lrrecpred  27856  fpwrelmap  32677  eulerpartlemgvv  34350  ballotlem2  34463  dffv5  35908  ptrest  37609  cnambfre  37658  cnvepresex  38314  pmapglb  39759  polval2N  39895  rngunsnply  43152  iocinico  43195