Theorem abid2 2900

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is used by:  csbid  3863  csbconstg  3869  csbie  3885  abss  3989  ssab  3990  abssi  3995  notab  4261  dfrab3  4266  notrab  4269  eusn  4690  uniintsn  4947  axrep6g  5245  csbexg  5266  imai  6077  dffv4  6890  orduniss2  7851  dfixp  8938  euen1b  9066  modom2  9254  pwfir  9319  infmap2  10305  ustfn  24533  ustn0  24552  lrrecse  28340  lrrecpred  28342  fpwrelmap  33378  eulerpartlemgvv  35061  ballotlem2  35174  abweex  35778  dffv5  36813  ptrest  38677  cnambfre  38726  cnvepresex  39408  pmapglb  40967  polval2N  41103  rngunsnply  44311  iocinico  44354