Theorem abid2 2898

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2739

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is used by:  csbid  3860  csbconstg  3866  csbie  3882  abss  4010  ssab  4011  abssi  4016  notab  4260  dfrab3  4265  notrab  4268  eusn  4691  uniintsn  4945  axrep6g  5243  csbexg  5264  imai  6072  dffv4  6882  orduniss2  7844  dfixp  8927  euen1b  9055  modom2  9243  pwfir  9308  infmap2  10295  ustfn  24521  ustn0  24540  lrrecse  28328  lrrecpred  28330  fpwrelmap  33325  eulerpartlemgvv  35008  ballotlem2  35121  abweex  35718  dffv5  36686  ptrest  38537  cnambfre  38586  cnvepresex  39268  pmapglb  40827  polval2N  40963  rngunsnply  44170  iocinico  44213