Theorem unieqi 4853

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

Syntax hints:   = wceq 1548  ∪ cuni 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842

This theorem is referenced by:  elunirab  4856  unisng  4859  unidif0  5291  unidif0OLD  5292  univ  5393  uniop  5459  dfiun3g  5917  op1sta  6180  op2nda  6183  dfdm2  6236  unixpid  6239  unisucs  6393  iotajust  6444  dfiota2  6446  cbviotaw  6452  cbviotavw  6453  cbviota  6454  sb8iota  6456  dffv4  6828  funfv2f  6920  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  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  20933  basdif0  22940  tgdif0  22979  neiptopuni  23117  restcls  23168  restntr  23169  pnrmopn  23330  cncmp  23379  discmp  23385  hauscmplem  23393  unisngl  23514  xkouni  23586  uptx  23612  ufildr  23918  ptcmplem3  24041  utop2nei  24237  utopreg  24239  zcld  24801  icccmp  24813  cncfcnvcn  24914  cnmpopc  24917  cnheibor  24944  evth  24948  evth2  24949  iunmbl  25542  voliun  25543  dvcnvrelem2  26007  ftc1  26031  aannenlem2  26317  bday1  27828  old0  27853  made0  27877  old1  27879  madeoldsuc  27899  isconstr  33932  circtopn  34033  locfinref  34037  zarmxt1  34076  tpr2rico  34108  cbvesum  34238  cbvesumv  34239  unibrsiga  34382  sxbrsigalem3  34468  dya2iocucvr  34480  sxbrsigalem1  34481  sibf0  34530  sibff  34532  sitgclg  34538  probfinmeasbALTV  34625  coinflipuniv  34678  fineqvnttrclse  35320  wevgblacfn  35352  cvmliftlem10  35537  dfon2lem7  36030  dfrdg2  36036  dfiota3  36164  dffv5  36165  dfrecs2  36193  dfrdg4  36194  ordcmp  36690  ttcuni  36756  bj-nuliotaALT  37426  mptsnun  37716  finxp1o  37769  ftc1cnnc  38074  cnvepima  38719  sn-iotalemcor  42724  onsucunitp  43833  dfom6  43990  refsum2cnlem1  45500  lptre2pt  46097  limclner  46108  limclr  46112  stoweidlem62  46519  fourierdlem42  46606  fourierdlem80  46643  fouriercnp  46683  qndenserrn  46756  salexct3  46799  salgencntex  46800  salgensscntex  46801  subsalsal  46816  0ome  46986  borelmbl  47093  mbfresmf  47196  cnfsmf  47197  incsmf  47199  smfmbfcex  47217  decsmf  47224  smfpimbor1lem2  47256  dftpos5  49378  ipoglb0  49498  setrec2  50199