MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abid2 Structured version   Visualization version   Unicode version

Theorem abid2 2573
Description: A simplification of class abstraction. Commuted form of abid1 2572. See comments there. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
abid2  |-  { x  |  x  e.  A }  =  A
Distinct variable group:    x, A

Proof of Theorem abid2
StepHypRef Expression
1 abid1 2572 . 2  |-  A  =  { x  |  x  e.  A }
21eqcomi 2460 1  |-  { x  |  x  e.  A }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444    e. wcel 1887   {cab 2437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447
This theorem is referenced by:  csbid  3371  abss  3498  ssab  3499  abssi  3504  notab  3713  dfrab3  3718  notrab  3720  eusn  4048  uniintsn  4272  iunid  4333  csbexg  4537  imai  5180  dffv4  5862  orduniss2  6660  dfixp  7524  euen1b  7640  modom2  7774  infmap2  8648  cshwsexa  12923  ustfn  21216  ustn0  21235  fpwrelmap  28318  eulerpartlemgvv  29209  ballotlem2  29321  dffv5  30691  ptrest  31939  cnambfre  31989  pmapglb  33335  polval2N  33471  rngunsnply  36039  iocinico  36096
  Copyright terms: Public domain W3C validator