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

Theorem unieqi 3837
Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
unieqi.1  |-  A  =  B
Assertion
Ref Expression
unieqi  |-  U. A  =  U. B

Proof of Theorem unieqi
StepHypRef Expression
1 unieqi.1 . 2  |-  A  =  B
2 unieq 3836 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2ax-mp 8 1  |-  U. A  =  U. B
Colors of variables: wff set class
Syntax hints:    = wceq 1623   U.cuni 3827
This theorem is referenced by:  elunirab  3840  unisn  3843  unidif0  4183  uniop  4269  unisuc  4468  univ  4565  ordunisuc  4623  dfiun3g  4931  op1sta  5154  op2nda  5157  dfdm2  5204  unixpid  5207  iotajust  5218  dfiota2  5220  cbviota  5224  sb8iota  5226  dffv4  5522  funfv2f  5588  funiunfv  5774  elunirn  5777  1st0  6126  2nd0  6127  unielxp  6158  brtpos0  6241  ovtpos  6249  riotauni  6311  recsfval  6397  tz7.44-3  6421  uniqs  6719  xpassen  6956  dffi3  7184  dfsup2  7195  dfsup2OLD  7196  dfsup3OLD  7197  r1limg  7443  jech9.3  7486  rankxplim2  7550  rankxplim3  7551  rankxpsuc  7552  dfac5lem2  7751  kmlem11  7786  cflim2  7889  fin23lem30  7968  fin23lem34  7972  itunisuc  8045  itunitc  8047  ituniiun  8048  ac6num  8106  rankcf  8399  dprd2da  15277  dmdprdsplit2lem  15280  lssuni  15697  basdif0  16691  tgdif0  16730  restcls  16911  restntr  16912  pnrmopn  17071  cncmp  17119  discmp  17125  hauscmplem  17133  xkouni  17294  uptx  17319  ufildr  17626  ptcmplem3  17748  zcld  18319  icccmp  18330  cncfcnvcn  18424  cnmpt2pc  18426  cnheibor  18453  evth  18457  evth2  18458  iunmbl  18910  voliun  18911  dvcnvrelem2  19365  ftc1  19389  aannenlem2  19709  cvmliftlem10  23236  dfon2lem7  23556  dfrdg2  23563  wfrlem12  23678  frrlem11  23704  dfiota3  23873  dffv5  23874  funpartfv  23894  dfrdg4  23899  bpolyval  24195  ordcmp  24297  repfuntw  24572  empos  24654  intopcoaconlem3b  24950  prdnei  24985  limptlimpr2lem1  24986  limptlimpr2lem2  24987  nolimf  25031  flfnein  25033  flfneic  25036  refsum2cnlem1  27120  stoweidlem62  27223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828
  Copyright terms: Public domain W3C validator