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  5298  unidif0OLD  5299  univ  5400  uniop  5465  dfiun3g  5919  op1sta  6185  op2nda  6188  dfdm2  6241  unixpid  6244  unisucs  6398  iotajust  6449  dfiota2  6451  cbviotaw  6457  cbviotavw  6458  cbviota  6459  sb8iota  6461  dffv4  6833  funfv2f  6925  funiunfv  7198  elunirnALT  7202  riotauni  7325  ordunisuc  7778  1st0  7943  2nd0  7944  unielxp  7975  brtpos0  8178  frrlem5  8235  frrlem8  8238  frrlem10  8240  dfrecs3  8307  recsfval  8315  tz7.44-3  8342  nlim1  8419  nlim2  8420  uniqs  8715  xpassen  9004  dffi3  9339  dfsup2  9352  sup00  9373  r1limg  9690  jech9.3  9733  rankxplim2  9799  rankxplim3  9800  rankxpsuc  9801  dfac5lem2  10041  kmlem11  10078  cflim2  10180  fin23lem30  10259  fin23lem34  10263  itunisuc  10336  itunitc  10338  ituniiun  10339  ac6num  10396  rankcf  10695  dprd2da  20014  dmdprdsplit2lem  20017  lssuni  20929  basdif0  22932  tgdif0  22971  neiptopuni  23109  restcls  23160  restntr  23161  pnrmopn  23322  cncmp  23371  discmp  23377  hauscmplem  23385  unisngl  23506  xkouni  23578  uptx  23604  ufildr  23910  ptcmplem3  24033  utop2nei  24229  utopreg  24231  zcld  24793  icccmp  24805  cncfcnvcn  24906  cnmpopc  24909  cnheibor  24936  evth  24940  evth2  24941  iunmbl  25534  voliun  25535  dvcnvrelem2  25999  ftc1  26023  aannenlem2  26310  bday1  27824  old0  27849  made0  27873  old1  27875  madeoldsuc  27895  isconstr  33900  circtopn  34001  locfinref  34005  zarmxt1  34044  tpr2rico  34076  cbvesum  34206  cbvesumv  34207  unibrsiga  34350  sxbrsigalem3  34436  dya2iocucvr  34448  sxbrsigalem1  34449  sibf0  34498  sibff  34500  sitgclg  34506  probfinmeasbALTV  34593  coinflipuniv  34646  fineqvnttrclse  35288  wevgblacfn  35311  cvmliftlem10  35496  dfon2lem7  35989  dfrdg2  35995  dfiota3  36123  dffv5  36124  dfrecs2  36152  dfrdg4  36153  ordcmp  36649  ttcuni  36715  bj-nuliotaALT  37385  mptsnun  37675  finxp1o  37728  ftc1cnnc  38033  cnvepima  38678  sn-iotalemcor  42683  onsucunitp  43825  dfom6  43982  refsum2cnlem1  45492  lptre2pt  46092  limclner  46103  limclr  46107  stoweidlem62  46514  fourierdlem42  46601  fourierdlem80  46638  fouriercnp  46678  qndenserrn  46751  salexct3  46794  salgencntex  46795  salgensscntex  46796  subsalsal  46811  0ome  46981  borelmbl  47088  mbfresmf  47191  cnfsmf  47192  incsmf  47194  smfmbfcex  47212  decsmf  47219  smfpimbor1lem2  47251  dftpos5  49367  ipoglb0  49487  setrec2  50188