Theorem unieqi 4863

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

Step	Hyp	Ref	Expression
1		unieqi.1	. 2 ⊢ 𝐴 = 𝐵
2		unieq 4862	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 = ∪ 𝐵

Syntax hints:   = wceq 1542  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  elunirab  4866  unisng  4869  unidif0  5295  univ  5396  uniop  5461  dfiun3g  5915  op1sta  6181  op2nda  6184  dfdm2  6237  unixpid  6240  unisucs  6394  iotajust  6445  dfiota2  6447  cbviotaw  6453  cbviotavw  6454  cbviota  6455  sb8iota  6457  dffv4  6829  funfv2f  6921  funiunfv  7194  elunirnALT  7198  riotauni  7321  ordunisuc  7774  1st0  7939  2nd0  7940  unielxp  7971  brtpos0  8174  frrlem5  8231  frrlem8  8234  frrlem10  8236  dfrecs3  8303  recsfval  8311  tz7.44-3  8338  nlim1  8415  nlim2  8416  uniqs  8711  xpassen  9000  dffi3  9335  dfsup2  9348  sup00  9369  r1limg  9684  jech9.3  9727  rankxplim2  9793  rankxplim3  9794  rankxpsuc  9795  dfac5lem2  10035  kmlem11  10072  cflim2  10174  fin23lem30  10253  fin23lem34  10257  itunisuc  10330  itunitc  10332  ituniiun  10333  ac6num  10390  rankcf  10689  dprd2da  20008  dmdprdsplit2lem  20011  lssuni  20923  basdif0  22926  tgdif0  22965  neiptopuni  23103  restcls  23154  restntr  23155  pnrmopn  23316  cncmp  23365  discmp  23371  hauscmplem  23379  unisngl  23500  xkouni  23572  uptx  23598  ufildr  23904  ptcmplem3  24027  utop2nei  24223  utopreg  24225  zcld  24787  icccmp  24799  cncfcnvcn  24900  cnmpopc  24903  cnheibor  24930  evth  24934  evth2  24935  iunmbl  25528  voliun  25529  dvcnvrelem2  25993  ftc1  26017  aannenlem2  26304  bday1  27818  old0  27843  made0  27867  old1  27869  madeoldsuc  27889  isconstr  33894  circtopn  33995  locfinref  33999  zarmxt1  34038  tpr2rico  34070  cbvesum  34200  cbvesumv  34201  unibrsiga  34344  sxbrsigalem3  34430  dya2iocucvr  34442  sxbrsigalem1  34443  sibf0  34492  sibff  34494  sitgclg  34500  probfinmeasbALTV  34587  coinflipuniv  34640  fineqvnttrclse  35282  wevgblacfn  35305  cvmliftlem10  35490  dfon2lem7  35983  dfrdg2  35989  dfiota3  36117  dffv5  36118  dfrecs2  36146  dfrdg4  36147  ordcmp  36643  ttcuni  36709  bj-nuliotaALT  37371  mptsnun  37659  finxp1o  37712  ftc1cnnc  38017  cnvepima  38662  sn-iotalemcor  42667  onsucunitp  43809  dfom6  43966  refsum2cnlem1  45476  lptre2pt  46076  limclner  46087  limclr  46091  stoweidlem62  46498  fourierdlem42  46585  fourierdlem80  46622  fouriercnp  46662  qndenserrn  46735  salexct3  46778  salgencntex  46779  salgensscntex  46780  subsalsal  46795  0ome  46965  borelmbl  47072  mbfresmf  47175  cnfsmf  47176  incsmf  47178  smfmbfcex  47196  decsmf  47203  smfpimbor1lem2  47235  dftpos5  49351  ipoglb0  49471  setrec2  50172