Theorem abid2 2901

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  {cab 2741

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  csbid  3864  csbconstg  3870  csbie  3886  abss  3990  ssab  3991  abssi  3996  notab  4262  dfrab3  4267  notrab  4270  eusn  4693  uniintsn  4950  axrep6g  5249  csbexg  5270  imai  6090  dffv4  6913  orduniss2  7878  dfixp  8965  euen1b  9093  modom2  9281  pwfir  9346  infmap2  10334  ustfn  24576  ustn0  24595  rngunsnply  26693  lrrecse  28385  lrrecpred  28387  fpwrelmap  33421  eulerpartlemgvv  35119  ballotlem2  35232  abweex  35842  dffv5  36901  ptrest  38805  cnambfre  38854  cnvepresex  39534  pmapglb  41093  polval2N  41229  iocinico  44475