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

Theorem unieqi 3967
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 3966 . 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 1649   U.cuni 3957
This theorem is referenced by:  elunirab  3970  unisn  3973  unidif0  4313  uniop  4400  unisuc  4598  univ  4694  ordunisuc  4752  dfiun3g  5062  op1sta  5291  op2nda  5294  dfdm2  5341  unixpid  5344  iotajust  5357  dfiota2  5359  cbviota  5363  sb8iota  5365  dffv4  5665  funfv2f  5731  funiunfv  5934  elunirn  5937  1st0  6292  2nd0  6293  unielxp  6324  brtpos0  6422  riotauni  6492  recsfval  6578  tz7.44-3  6602  uniqs  6900  xpassen  7138  dffi3  7371  dfsup2  7382  dfsup2OLD  7383  dfsup3OLD  7384  r1limg  7630  jech9.3  7673  rankxplim2  7737  rankxplim3  7738  rankxpsuc  7739  dfac5lem2  7938  kmlem11  7973  cflim2  8076  fin23lem30  8155  fin23lem34  8159  itunisuc  8232  itunitc  8234  ituniiun  8235  ac6num  8292  rankcf  8585  dprd2da  15527  dmdprdsplit2lem  15530  lssuni  15943  basdif0  16941  tgdif0  16980  neiptopuni  17117  restcls  17167  restntr  17168  pnrmopn  17329  cncmp  17377  discmp  17383  hauscmplem  17391  xkouni  17552  uptx  17578  ufildr  17884  ptcmplem3  18006  utop2nei  18201  utopreg  18203  zcld  18715  icccmp  18727  cncfcnvcn  18822  cnmpt2pc  18824  cnheibor  18851  evth  18855  evth2  18856  iunmbl  19314  voliun  19315  dvcnvrelem2  19769  ftc1  19793  aannenlem2  20113  tpr2rico  24114  cbvesum  24234  unibrsiga  24336  sxbrsigalem3  24416  dya2iocucvr  24428  sxbrsigalem1  24429  probfinmeasbOLD  24465  coinflipuniv  24518  cvmliftlem10  24760  dfon2lem7  25169  dfrdg2  25176  wfrlem12  25291  frrlem11  25317  dfiota3  25486  dffv5  25487  dfrdg4  25513  bpolyval  25809  ordcmp  25911  ftc1cnnc  25979  refsum2cnlem1  27376  stoweidlem62  27479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-uni 3958
  Copyright terms: Public domain W3C validator