Theorem abid2 2902

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {cab 2743

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is used by:  csbid  3867  csbconstg  3873  csbie  3889  abss  4017  ssab  4018  abssi  4023  notab  4267  dfrab3  4272  notrab  4275  eusn  4698  uniintsn  4952  axrep6g  5253  csbexg  5275  imai  6078  dffv4  6882  orduniss2  7835  dfixp  8903  euen1b  9031  modom2  9219  pwfir  9283  infmap2  10216  ustfn  24412  ustn0  24431  lrrecse  28188  lrrecpred  28190  fpwrelmap  33150  eulerpartlemgvv  34833  ballotlem2  34946  dffv5  36453  ptrest  38329  cnambfre  38378  cnvepresex  39045  pmapglb  40604  polval2N  40740  rngunsnply  43956  iocinico  43999