Theorem abid2 2897

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

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  5245  csbexg  5267  imai  6070  dffv4  6876  orduniss2  7830  dfixp  8909  euen1b  9037  modom2  9225  pwfir  9289  infmap2  10222  ustfn  24431  ustn0  24450  lrrecse  28210  lrrecpred  28212  fpwrelmap  33207  eulerpartlemgvv  34890  ballotlem2  35003  dffv5  36504  ptrest  38371  cnambfre  38420  cnvepresex  39087  pmapglb  40646  polval2N  40782  rngunsnply  44013  iocinico  44056