Theorem unieqi 4879

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

Syntax hints:   = wceq 1540  ∪ cuni 4867

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  elunirab  4882  unisng  4885  unidif0  5310  univ  5406  uniop  5470  dfiun3g  5920  op1sta  6186  op2nda  6189  dfdm2  6242  unixpid  6245  unisucs  6399  iotajust  6451  dfiota2  6453  cbviotaw  6459  cbviotavw  6460  cbviota  6461  sb8iota  6463  dffv4  6837  funfv2f  6932  funiunfv  7204  elunirnALT  7208  riotauni  7332  ordunisuc  7787  1st0  7953  2nd0  7954  unielxp  7985  brtpos0  8189  frrlem5  8246  frrlem8  8249  frrlem10  8251  dfrecs3  8318  recsfval  8326  tz7.44-3  8353  nlim1  8430  nlim2  8431  uniqs  8724  xpassen  9012  dffi3  9358  dfsup2  9371  sup00  9392  r1limg  9700  jech9.3  9743  rankxplim2  9809  rankxplim3  9810  rankxpsuc  9811  dfac5lem2  10053  kmlem11  10090  cflim2  10192  fin23lem30  10271  fin23lem34  10275  itunisuc  10348  itunitc  10350  ituniiun  10351  ac6num  10408  rankcf  10706  dprd2da  19958  dmdprdsplit2lem  19961  lssuni  20877  basdif0  22873  tgdif0  22912  neiptopuni  23050  restcls  23101  restntr  23102  pnrmopn  23263  cncmp  23312  discmp  23318  hauscmplem  23326  unisngl  23447  xkouni  23519  uptx  23545  ufildr  23851  ptcmplem3  23974  utop2nei  24171  utopreg  24173  zcld  24735  icccmp  24747  cncfcnvcn  24852  cnmpopc  24855  cnheibor  24887  evth  24891  evth2  24892  iunmbl  25487  voliun  25488  dvcnvrelem2  25956  ftc1  25982  aannenlem2  26270  bday1s  27780  old0  27804  made0  27822  old1  27824  madeoldsuc  27834  zs12bday  28396  isconstr  33719  circtopn  33820  locfinref  33824  zarmxt1  33863  tpr2rico  33895  cbvesum  34025  cbvesumv  34026  unibrsiga  34169  sxbrsigalem3  34256  dya2iocucvr  34268  sxbrsigalem1  34269  sibf0  34318  sibff  34320  sitgclg  34326  probfinmeasbALTV  34413  coinflipuniv  34466  wevgblacfn  35089  cvmliftlem10  35274  dfon2lem7  35770  dfrdg2  35776  dfiota3  35904  dffv5  35905  dfrecs2  35931  dfrdg4  35932  ordcmp  36428  bj-nuliotaALT  37039  mptsnun  37320  finxp1o  37373  ftc1cnnc  37679  cnvepima  38312  sn-iotalemcor  42203  onsucunitp  43355  dfom6  43513  refsum2cnlem1  45024  lptre2pt  45631  limclner  45642  limclr  45646  stoweidlem62  46053  fourierdlem42  46140  fourierdlem80  46177  fouriercnp  46217  qndenserrn  46290  salexct3  46333  salgencntex  46334  salgensscntex  46335  subsalsal  46350  0ome  46520  borelmbl  46627  mbfresmf  46730  cnfsmf  46731  incsmf  46733  smfmbfcex  46751  decsmf  46758  smfpimbor1lem2  46790  dftpos5  48855  ipoglb0  48975  setrec2  49677