Theorem abid2 2867

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  csbid  3883  csbconstg  3889  csbie  3905  abss  4034  ssab  4035  abssi  4041  notab  4285  dfrab3  4290  notrab  4293  eusn  4702  uniintsn  4957  iunidOLD  5033  axrep6g  5253  csbexg  5273  imai  6053  dffv4  6862  orduniss2  7816  dfixp  8876  euen1b  9005  modom2  9210  pwfir  9284  infmap2  10188  cshwsexaOLD  14800  ustfn  24095  ustn0  24114  lrrecse  27856  lrrecpred  27858  fpwrelmap  32664  eulerpartlemgvv  34375  ballotlem2  34488  dffv5  35909  ptrest  37610  cnambfre  37659  cnvepresex  38319  pmapglb  39756  polval2N  39892  rngunsnply  43130  iocinico  43173