Theorem unieqi 4849

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

Syntax hints:   = wceq 1539  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  elunirab  4852  unisng  4857  unidif0  5277  univ  5361  uniop  5423  dfiun3g  5862  op1sta  6117  op2nda  6120  dfdm2  6173  unixpid  6176  unisuc  6327  iotajust  6375  dfiota2  6377  cbviotaw  6383  cbviotavw  6384  cbviota  6386  sb8iota  6388  dffv4  6753  funfv2f  6839  funiunfv  7103  elunirnALT  7107  riotauni  7218  ordunisuc  7654  1st0  7810  2nd0  7811  unielxp  7842  brtpos0  8020  frrlem5  8077  frrlem8  8080  frrlem10  8082  dfwrecsOLD  8100  dfrecs3  8174  dfrecs3OLD  8175  recsfval  8183  tz7.44-3  8210  uniqs  8524  xpassen  8806  dffi3  9120  dfsup2  9133  sup00  9153  r1limg  9460  jech9.3  9503  rankxplim2  9569  rankxplim3  9570  rankxpsuc  9571  dfac5lem2  9811  kmlem11  9847  cflim2  9950  fin23lem30  10029  fin23lem34  10033  itunisuc  10106  itunitc  10108  ituniiun  10109  ac6num  10166  rankcf  10464  dprd2da  19560  dmdprdsplit2lem  19563  lssuni  20116  basdif0  22011  tgdif0  22050  neiptopuni  22189  restcls  22240  restntr  22241  pnrmopn  22402  cncmp  22451  discmp  22457  hauscmplem  22465  unisngl  22586  xkouni  22658  uptx  22684  ufildr  22990  ptcmplem3  23113  utop2nei  23310  utopreg  23312  zcld  23882  icccmp  23894  cncfcnvcn  23994  cnmpopc  23997  cnheibor  24024  evth  24028  evth2  24029  iunmbl  24622  voliun  24623  dvcnvrelem2  25087  ftc1  25111  aannenlem2  25394  circtopn  31689  locfinref  31693  zarmxt1  31732  tpr2rico  31764  cbvesum  31910  unibrsiga  32054  sxbrsigalem3  32139  dya2iocucvr  32151  sxbrsigalem1  32152  sibf0  32201  sibff  32203  sitgclg  32209  probfinmeasbALTV  32296  coinflipuniv  32348  cvmliftlem10  33156  dfon2lem7  33671  dfrdg2  33677  bday1s  33952  old0  33970  made0  33984  madeoldsuc  33994  dfiota3  34152  dffv5  34153  dfrecs2  34179  dfrdg4  34180  ordcmp  34563  bj-nuliotaALT  35156  mptsnun  35437  finxp1o  35490  ftc1cnnc  35776  uniqsALTV  36391  cnvepima  36399  sn-iotalemcor  40118  dfom6  41036  refsum2cnlem1  42469  lptre2pt  43071  limclner  43082  limclr  43086  stoweidlem62  43493  fourierdlem42  43580  fourierdlem80  43617  fouriercnp  43657  qndenserrn  43730  salexct3  43771  salgencntex  43772  salgensscntex  43773  subsalsal  43788  0ome  43957  borelmbl  44064  mbfresmf  44162  cnfsmf  44163  incsmf  44165  smfmbfcex  44182  decsmf  44189  smfpimbor1lem2  44220  ipoglb0  46168  setrec2  46287