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

Theorem unieqi 4017
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 4016 . 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 1652   U.cuni 4007
This theorem is referenced by:  elunirab  4020  unisn  4023  unidif0  4364  uniop  4451  unisuc  4649  univ  4746  ordunisuc  4804  dfiun3g  5114  op1sta  5343  op2nda  5346  dfdm2  5393  unixpid  5396  iotajust  5409  dfiota2  5411  cbviota  5415  sb8iota  5417  dffv4  5717  funfv2f  5784  funiunfv  5987  elunirn  5990  1st0  6345  2nd0  6346  unielxp  6377  brtpos0  6478  riotauni  6548  recsfval  6634  tz7.44-3  6658  uniqs  6956  xpassen  7194  dffi3  7428  dfsup2  7439  dfsup2OLD  7440  dfsup3OLD  7441  r1limg  7689  jech9.3  7732  rankxplim2  7796  rankxplim3  7797  rankxpsuc  7798  dfac5lem2  7997  kmlem11  8032  cflim2  8135  fin23lem30  8214  fin23lem34  8218  itunisuc  8291  itunitc  8293  ituniiun  8294  ac6num  8351  rankcf  8644  dprd2da  15592  dmdprdsplit2lem  15595  lssuni  16008  basdif0  17010  tgdif0  17049  neiptopuni  17186  restcls  17237  restntr  17238  pnrmopn  17399  cncmp  17447  discmp  17453  hauscmplem  17461  xkouni  17623  uptx  17649  ufildr  17955  ptcmplem3  18077  utop2nei  18272  utopreg  18274  zcld  18836  icccmp  18848  cncfcnvcn  18943  cnmpt2pc  18945  cnheibor  18972  evth  18976  evth2  18977  iunmbl  19439  voliun  19440  dvcnvrelem2  19894  ftc1  19918  aannenlem2  20238  tpr2rico  24302  cbvesum  24430  unibrsiga  24532  sxbrsigalem3  24614  dya2iocucvr  24626  sxbrsigalem1  24627  sibf0  24641  sibff  24643  sibfof  24646  sitgclg  24648  probfinmeasbOLD  24678  coinflipuniv  24731  cvmliftlem10  24973  dfon2lem7  25408  dfrdg2  25415  frrlem11  25586  dfiota3  25760  dffv5  25761  dfrdg4  25787  ordcmp  26189  ftc1cnnc  26269  refsum2cnlem1  27675  stoweidlem62  27778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-uni 4008
  Copyright terms: Public domain W3C validator