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

Theorem unieqi 4839
Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
unieqi.1 𝐴 = 𝐵
Assertion
Ref Expression
unieqi 𝐴 = 𝐵

Proof of Theorem unieqi
StepHypRef Expression
1 unieqi.1 . 2 𝐴 = 𝐵
2 unieq 4838 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rex 3141  df-uni 4831
This theorem is referenced by:  elunirab  4842  unisng  4845  unidif0  5251  univ  5334  uniop  5396  dfiun3g  5828  op1sta  6075  op2nda  6078  dfdm2  6125  unixpid  6128  unisuc  6260  iotajust  6306  dfiota2  6308  cbviotaw  6314  cbviota  6316  sb8iota  6318  dffv4  6660  funfv2f  6745  funiunfv  6998  elunirnALT  7002  riotauni  7109  ordunisuc  7536  1st0  7684  2nd0  7685  unielxp  7716  brtpos0  7888  dfrecs3  7998  recsfval  8006  tz7.44-3  8033  uniqs  8346  xpassen  8599  dffi3  8883  dfsup2  8896  sup00  8916  r1limg  9188  jech9.3  9231  rankxplim2  9297  rankxplim3  9298  rankxpsuc  9299  dfac5lem2  9538  kmlem11  9574  cflim2  9673  fin23lem30  9752  fin23lem34  9756  itunisuc  9829  itunitc  9831  ituniiun  9832  ac6num  9889  rankcf  10187  dprd2da  19093  dmdprdsplit2lem  19096  lssuni  19640  basdif0  21489  tgdif0  21528  neiptopuni  21666  restcls  21717  restntr  21718  pnrmopn  21879  cncmp  21928  discmp  21934  hauscmplem  21942  unisngl  22063  xkouni  22135  uptx  22161  ufildr  22467  ptcmplem3  22590  utop2nei  22786  utopreg  22788  zcld  23348  icccmp  23360  cncfcnvcn  23456  cnmpopc  23459  cnheibor  23486  evth  23490  evth2  23491  iunmbl  24081  voliun  24082  dvcnvrelem2  24542  ftc1  24566  aannenlem2  24845  circtopn  31000  locfinref  31004  tpr2rico  31054  cbvesum  31200  unibrsiga  31344  sxbrsigalem3  31429  dya2iocucvr  31441  sxbrsigalem1  31442  sibf0  31491  sibff  31493  sitgclg  31499  probfinmeasbALTV  31586  coinflipuniv  31638  cvmliftlem10  32438  dfon2lem7  32931  dfrdg2  32937  frrlem5  33024  frrlem8  33027  frrlem10  33029  noetalem4  33117  dfiota3  33281  dffv5  33282  dfrecs2  33308  dfrdg4  33309  ordcmp  33692  bj-nuliotaALT  34245  mptsnun  34502  finxp1o  34555  ftc1cnnc  34847  uniqsALTV  35467  cnvepima  35475  dfom6  39776  refsum2cnlem1  41171  lptre2pt  41797  limclner  41808  limclr  41812  stoweidlem62  42224  fourierdlem42  42311  fourierdlem80  42348  fouriercnp  42388  qndenserrn  42461  salexct3  42502  salgencntex  42503  salgensscntex  42504  subsalsal  42519  0ome  42688  borelmbl  42795  mbfresmf  42893  cnfsmf  42894  incsmf  42896  smfmbfcex  42913  decsmf  42920  smfpimbor1lem2  42951  setrec2  44726
  Copyright terms: Public domain W3C validator