Theorem unieqi 4923

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

Syntax hints:   = wceq 1536  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912

This theorem is referenced by:  elunirab  4926  unisng  4929  unidif0  5365  univ  5461  uniop  5524  dfiun3g  5980  op1sta  6246  op2nda  6249  dfdm2  6302  unixpid  6305  unisucs  6462  iotajust  6514  dfiota2  6516  cbviotaw  6522  cbviotavw  6523  cbviota  6524  sb8iota  6526  dffv4  6903  funfv2f  6997  funiunfv  7267  elunirnALT  7271  riotauni  7393  ordunisuc  7851  1st0  8018  2nd0  8019  unielxp  8050  brtpos0  8256  frrlem5  8313  frrlem8  8316  frrlem10  8318  dfwrecsOLD  8336  dfrecs3  8410  dfrecs3OLD  8411  recsfval  8419  tz7.44-3  8446  nlim1  8525  nlim2  8526  uniqs  8815  xpassen  9104  dffi3  9468  dfsup2  9481  sup00  9501  r1limg  9808  jech9.3  9851  rankxplim2  9917  rankxplim3  9918  rankxpsuc  9919  dfac5lem2  10161  kmlem11  10198  cflim2  10300  fin23lem30  10379  fin23lem34  10383  itunisuc  10456  itunitc  10458  ituniiun  10459  ac6num  10516  rankcf  10814  dprd2da  20076  dmdprdsplit2lem  20079  lssuni  20954  basdif0  22975  tgdif0  23014  neiptopuni  23153  restcls  23204  restntr  23205  pnrmopn  23366  cncmp  23415  discmp  23421  hauscmplem  23429  unisngl  23550  xkouni  23622  uptx  23648  ufildr  23954  ptcmplem3  24077  utop2nei  24274  utopreg  24276  zcld  24848  icccmp  24860  cncfcnvcn  24965  cnmpopc  24968  cnheibor  25000  evth  25004  evth2  25005  iunmbl  25601  voliun  25602  dvcnvrelem2  26071  ftc1  26097  aannenlem2  26385  bday1s  27890  old0  27912  made0  27926  old1  27928  madeoldsuc  27937  zs12bday  28438  circtopn  33797  locfinref  33801  zarmxt1  33840  tpr2rico  33872  cbvesum  34022  cbvesumv  34023  unibrsiga  34166  sxbrsigalem3  34253  dya2iocucvr  34265  sxbrsigalem1  34266  sibf0  34315  sibff  34317  sitgclg  34323  probfinmeasbALTV  34410  coinflipuniv  34462  wevgblacfn  35092  cvmliftlem10  35278  dfon2lem7  35770  dfrdg2  35776  dfiota3  35904  dffv5  35905  dfrecs2  35931  dfrdg4  35932  ordcmp  36429  bj-nuliotaALT  37040  mptsnun  37321  finxp1o  37374  ftc1cnnc  37678  uniqsALTV  38310  cnvepima  38318  sn-iotalemcor  42239  onsucunitp  43362  dfom6  43520  refsum2cnlem1  44974  lptre2pt  45595  limclner  45606  limclr  45610  stoweidlem62  46017  fourierdlem42  46104  fourierdlem80  46141  fouriercnp  46181  qndenserrn  46254  salexct3  46297  salgencntex  46298  salgensscntex  46299  subsalsal  46314  0ome  46484  borelmbl  46591  mbfresmf  46694  cnfsmf  46695  incsmf  46697  smfmbfcex  46715  decsmf  46722  smfpimbor1lem2  46754  ipoglb0  48782  setrec2  48925