Theorem abid2 2866

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  csbid  3877  csbconstg  3883  csbie  3899  abss  4028  ssab  4029  abssi  4035  notab  4279  dfrab3  4284  notrab  4287  eusn  4696  uniintsn  4951  iunidOLD  5027  axrep6g  5247  csbexg  5267  imai  6047  dffv4  6857  orduniss2  7810  dfixp  8874  euen1b  9001  modom2  9198  pwfir  9272  infmap2  10176  cshwsexaOLD  14796  ustfn  24095  ustn0  24114  lrrecse  27855  lrrecpred  27857  fpwrelmap  32662  eulerpartlemgvv  34373  ballotlem2  34486  dffv5  35907  ptrest  37608  cnambfre  37657  cnvepresex  38313  pmapglb  39759  polval2N  39895  rngunsnply  43151  iocinico  43194