Theorem unieqi 4874

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 4873	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 = ∪ 𝐵

Syntax hints:   = wceq 1542  ∪ cuni 4862

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863

This theorem is referenced by:  elunirab  4877  unisng  4880  unidif0  5304  univ  5398  uniop  5462  dfiun3g  5916  op1sta  6182  op2nda  6185  dfdm2  6238  unixpid  6241  unisucs  6395  iotajust  6446  dfiota2  6448  cbviotaw  6454  cbviotavw  6455  cbviota  6456  sb8iota  6458  dffv4  6830  funfv2f  6922  funiunfv  7194  elunirnALT  7198  riotauni  7321  ordunisuc  7774  1st0  7939  2nd0  7940  unielxp  7971  brtpos0  8175  frrlem5  8232  frrlem8  8235  frrlem10  8237  dfrecs3  8304  recsfval  8312  tz7.44-3  8339  nlim1  8416  nlim2  8417  uniqs  8712  xpassen  9001  dffi3  9336  dfsup2  9349  sup00  9370  r1limg  9685  jech9.3  9728  rankxplim2  9794  rankxplim3  9795  rankxpsuc  9796  dfac5lem2  10036  kmlem11  10073  cflim2  10175  fin23lem30  10254  fin23lem34  10258  itunisuc  10331  itunitc  10333  ituniiun  10334  ac6num  10391  rankcf  10690  dprd2da  19975  dmdprdsplit2lem  19978  lssuni  20892  basdif0  22899  tgdif0  22938  neiptopuni  23076  restcls  23127  restntr  23128  pnrmopn  23289  cncmp  23338  discmp  23344  hauscmplem  23352  unisngl  23473  xkouni  23545  uptx  23571  ufildr  23877  ptcmplem3  24000  utop2nei  24196  utopreg  24198  zcld  24760  icccmp  24772  cncfcnvcn  24877  cnmpopc  24880  cnheibor  24912  evth  24916  evth2  24917  iunmbl  25512  voliun  25513  dvcnvrelem2  25981  ftc1  26007  aannenlem2  26295  bday1s  27810  old0  27835  made0  27853  old1  27855  madeoldsuc  27865  isconstr  33872  circtopn  33973  locfinref  33977  zarmxt1  34016  tpr2rico  34048  cbvesum  34178  cbvesumv  34179  unibrsiga  34322  sxbrsigalem3  34408  dya2iocucvr  34420  sxbrsigalem1  34421  sibf0  34470  sibff  34472  sitgclg  34478  probfinmeasbALTV  34565  coinflipuniv  34618  fineqvnttrclse  35259  wevgblacfn  35282  cvmliftlem10  35467  dfon2lem7  35960  dfrdg2  35966  dfiota3  36094  dffv5  36095  dfrecs2  36123  dfrdg4  36124  ordcmp  36620  bj-nuliotaALT  37232  mptsnun  37513  finxp1o  37566  ftc1cnnc  37862  cnvepima  38507  sn-iotalemcor  42516  onsucunitp  43652  dfom6  43809  refsum2cnlem1  45319  lptre2pt  45921  limclner  45932  limclr  45936  stoweidlem62  46343  fourierdlem42  46430  fourierdlem80  46467  fouriercnp  46507  qndenserrn  46580  salexct3  46623  salgencntex  46624  salgensscntex  46625  subsalsal  46640  0ome  46810  borelmbl  46917  mbfresmf  47020  cnfsmf  47021  incsmf  47023  smfmbfcex  47041  decsmf  47048  smfpimbor1lem2  47080  dftpos5  49156  ipoglb0  49276  setrec2  49977