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

Theorem unieqi 4416
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 4415 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480   cuni 4407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4408
This theorem is referenced by:  elunirab  4419  unisn  4422  unidif0  4803  univ  4885  uniop  4942  dfiun3g  5343  op1sta  5581  op2nda  5584  dfdm2  5631  unixpid  5634  unisuc  5765  iotajust  5814  dfiota2  5816  cbviota  5820  sb8iota  5822  dffv4  6150  funfv2f  6229  funiunfv  6466  elunirnALT  6470  riotauni  6577  ordunisuc  6986  1st0  7126  2nd0  7127  unielxp  7156  brtpos0  7311  dfrecs3  7421  recsfval  7429  tz7.44-3  7456  uniqs  7759  xpassen  8006  dffi3  8289  dfsup2  8302  sup00  8322  r1limg  8586  jech9.3  8629  rankxplim2  8695  rankxplim3  8696  rankxpsuc  8697  dfac5lem2  8899  kmlem11  8934  cflim2  9037  fin23lem30  9116  fin23lem34  9120  itunisuc  9193  itunitc  9195  ituniiun  9196  ac6num  9253  rankcf  9551  dprd2da  18373  dmdprdsplit2lem  18376  lssuni  18872  basdif0  20681  tgdif0  20720  neiptopuni  20857  restcls  20908  restntr  20909  pnrmopn  21070  cncmp  21118  discmp  21124  hauscmplem  21132  unisngl  21253  xkouni  21325  uptx  21351  ufildr  21658  ptcmplem3  21781  utop2nei  21977  utopreg  21979  zcld  22539  icccmp  22551  cncfcnvcn  22647  cnmpt2pc  22650  cnheibor  22677  evth  22681  evth2  22682  iunmbl  23244  voliun  23245  dvcnvrelem2  23702  ftc1  23726  aannenlem2  24005  circtopn  29710  locfinref  29714  tpr2rico  29764  cbvesum  29909  unibrsiga  30054  sxbrsigalem3  30139  dya2iocucvr  30151  sxbrsigalem1  30152  sibf0  30201  sibff  30203  sitgclg  30209  probfinmeasbOLD  30295  coinflipuniv  30348  cvmliftlem10  31019  dfon2lem7  31430  dfrdg2  31437  frrlem11  31528  dfiota3  31707  dffv5  31708  dfrecs2  31734  dfrdg4  31735  ordcmp  32123  bj-nuliotaALT  32702  mptsnun  32853  finxp1o  32896  ftc1cnnc  33151  refsum2cnlem1  38714  lptre2pt  39304  limclner  39315  limclr  39319  stoweidlem62  39612  fourierdlem42  39699  fourierdlem80  39736  fouriercnp  39776  qndenserrn  39852  salexct3  39893  salgencntex  39894  salgensscntex  39895  subsalsal  39910  0ome  40076  borelmbl  40183  mbfresmf  40281  cnfsmf  40282  incsmf  40284  smfmbfcex  40301  decsmf  40308  smfpimbor1lem2  40339  setrec2  41761
  Copyright terms: Public domain W3C validator