Theorem unieqi 4876

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

Syntax hints:   = wceq 1542  ∪ cuni 4864

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 3443  df-ss 3919  df-uni 4865

This theorem is referenced by:  elunirab  4879  unisng  4882  unidif0  5306  univ  5400  uniop  5464  dfiun3g  5918  op1sta  6184  op2nda  6187  dfdm2  6240  unixpid  6243  unisucs  6397  iotajust  6448  dfiota2  6450  cbviotaw  6456  cbviotavw  6457  cbviota  6458  sb8iota  6460  dffv4  6832  funfv2f  6924  funiunfv  7196  elunirnALT  7200  riotauni  7323  ordunisuc  7776  1st0  7941  2nd0  7942  unielxp  7973  brtpos0  8177  frrlem5  8234  frrlem8  8237  frrlem10  8239  dfrecs3  8306  recsfval  8314  tz7.44-3  8341  nlim1  8418  nlim2  8419  uniqs  8714  xpassen  9003  dffi3  9338  dfsup2  9351  sup00  9372  r1limg  9687  jech9.3  9730  rankxplim2  9796  rankxplim3  9797  rankxpsuc  9798  dfac5lem2  10038  kmlem11  10075  cflim2  10177  fin23lem30  10256  fin23lem34  10260  itunisuc  10333  itunitc  10335  ituniiun  10336  ac6num  10393  rankcf  10692  dprd2da  19977  dmdprdsplit2lem  19980  lssuni  20894  basdif0  22901  tgdif0  22940  neiptopuni  23078  restcls  23129  restntr  23130  pnrmopn  23291  cncmp  23340  discmp  23346  hauscmplem  23354  unisngl  23475  xkouni  23547  uptx  23573  ufildr  23879  ptcmplem3  24002  utop2nei  24198  utopreg  24200  zcld  24762  icccmp  24774  cncfcnvcn  24879  cnmpopc  24882  cnheibor  24914  evth  24918  evth2  24919  iunmbl  25514  voliun  25515  dvcnvrelem2  25983  ftc1  26009  aannenlem2  26297  bday1  27814  old0  27839  made0  27863  old1  27865  madeoldsuc  27885  isconstr  33895  circtopn  33996  locfinref  34000  zarmxt1  34039  tpr2rico  34071  cbvesum  34201  cbvesumv  34202  unibrsiga  34345  sxbrsigalem3  34431  dya2iocucvr  34443  sxbrsigalem1  34444  sibf0  34493  sibff  34495  sitgclg  34501  probfinmeasbALTV  34588  coinflipuniv  34641  fineqvnttrclse  35282  wevgblacfn  35305  cvmliftlem10  35490  dfon2lem7  35983  dfrdg2  35989  dfiota3  36117  dffv5  36118  dfrecs2  36146  dfrdg4  36147  ordcmp  36643  bj-nuliotaALT  37261  mptsnun  37546  finxp1o  37599  ftc1cnnc  37895  cnvepima  38540  sn-iotalemcor  42546  onsucunitp  43682  dfom6  43839  refsum2cnlem1  45349  lptre2pt  45951  limclner  45962  limclr  45966  stoweidlem62  46373  fourierdlem42  46460  fourierdlem80  46497  fouriercnp  46537  qndenserrn  46610  salexct3  46653  salgencntex  46654  salgensscntex  46655  subsalsal  46670  0ome  46840  borelmbl  46947  mbfresmf  47050  cnfsmf  47051  incsmf  47053  smfmbfcex  47071  decsmf  47078  smfpimbor1lem2  47110  dftpos5  49186  ipoglb0  49306  setrec2  50007