Theorem abid2 2871

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808

This theorem is referenced by:  csbid  3892  csbconstg  3898  csbie  3914  abss  4043  ssab  4044  abssi  4050  notab  4294  dfrab3  4299  notrab  4302  eusn  4710  uniintsn  4965  iunidOLD  5041  axrep6g  5270  csbexg  5290  imai  6072  dffv4  6882  orduniss2  7834  dfixp  8920  euen1b  9049  modom2  9262  pwfir  9336  infmap2  10238  cshwsexaOLD  14844  ustfn  24155  ustn0  24174  lrrecse  27910  lrrecpred  27912  fpwrelmap  32671  eulerpartlemgvv  34312  ballotlem2  34425  dffv5  35859  ptrest  37560  cnambfre  37609  cnvepresex  38269  pmapglb  39706  polval2N  39842  rngunsnply  43119  iocinico  43162