Theorem unieqi 4886

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

Syntax hints:   = wceq 1540  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  elunirab  4889  unisng  4892  unidif0  5318  univ  5414  uniop  5478  dfiun3g  5934  op1sta  6201  op2nda  6204  dfdm2  6257  unixpid  6260  unisucs  6414  iotajust  6466  dfiota2  6468  cbviotaw  6474  cbviotavw  6475  cbviota  6476  sb8iota  6478  dffv4  6858  funfv2f  6953  funiunfv  7225  elunirnALT  7229  riotauni  7353  ordunisuc  7810  1st0  7977  2nd0  7978  unielxp  8009  brtpos0  8215  frrlem5  8272  frrlem8  8275  frrlem10  8277  dfrecs3  8344  recsfval  8352  tz7.44-3  8379  nlim1  8456  nlim2  8457  uniqs  8750  xpassen  9040  dffi3  9389  dfsup2  9402  sup00  9423  r1limg  9731  jech9.3  9774  rankxplim2  9840  rankxplim3  9841  rankxpsuc  9842  dfac5lem2  10084  kmlem11  10121  cflim2  10223  fin23lem30  10302  fin23lem34  10306  itunisuc  10379  itunitc  10381  ituniiun  10382  ac6num  10439  rankcf  10737  dprd2da  19981  dmdprdsplit2lem  19984  lssuni  20852  basdif0  22847  tgdif0  22886  neiptopuni  23024  restcls  23075  restntr  23076  pnrmopn  23237  cncmp  23286  discmp  23292  hauscmplem  23300  unisngl  23421  xkouni  23493  uptx  23519  ufildr  23825  ptcmplem3  23948  utop2nei  24145  utopreg  24147  zcld  24709  icccmp  24721  cncfcnvcn  24826  cnmpopc  24829  cnheibor  24861  evth  24865  evth2  24866  iunmbl  25461  voliun  25462  dvcnvrelem2  25930  ftc1  25956  aannenlem2  26244  bday1s  27750  old0  27774  made0  27792  old1  27794  madeoldsuc  27803  zs12bday  28350  isconstr  33733  circtopn  33834  locfinref  33838  zarmxt1  33877  tpr2rico  33909  cbvesum  34039  cbvesumv  34040  unibrsiga  34183  sxbrsigalem3  34270  dya2iocucvr  34282  sxbrsigalem1  34283  sibf0  34332  sibff  34334  sitgclg  34340  probfinmeasbALTV  34427  coinflipuniv  34480  wevgblacfn  35103  cvmliftlem10  35288  dfon2lem7  35784  dfrdg2  35790  dfiota3  35918  dffv5  35919  dfrecs2  35945  dfrdg4  35946  ordcmp  36442  bj-nuliotaALT  37053  mptsnun  37334  finxp1o  37387  ftc1cnnc  37693  cnvepima  38326  sn-iotalemcor  42217  onsucunitp  43369  dfom6  43527  refsum2cnlem1  45038  lptre2pt  45645  limclner  45656  limclr  45660  stoweidlem62  46067  fourierdlem42  46154  fourierdlem80  46191  fouriercnp  46231  qndenserrn  46304  salexct3  46347  salgencntex  46348  salgensscntex  46349  subsalsal  46364  0ome  46534  borelmbl  46641  mbfresmf  46744  cnfsmf  46745  incsmf  46747  smfmbfcex  46765  decsmf  46772  smfpimbor1lem2  46804  dftpos5  48866  ipoglb0  48986  setrec2  49688