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 1562  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868

This theorem is referenced by:  elunirab  4882  unisng  4885  unidif0  5318  unidif0OLD  5319  univ  5420  uniop  5486  dfiun3g  5946  op1sta  6214  op2nda  6217  dfdm2  6270  unixpid  6273  unisucs  6427  iotajust  6478  dfiota2  6480  cbviotaw  6486  cbviotavw  6487  cbviota  6488  sb8iota  6490  dffv4  6866  funfv2f  6958  funiunfv  7234  elunirnALT  7238  riotauni  7361  ordunisuc  7814  1st0  7978  2nd0  7979  unielxp  8010  brtpos0  8215  frrlem5  8273  frrlem8  8276  frrlem10  8278  dfrecs3  8345  recsfval  8353  tz7.44-3  8381  nlim1  8460  nlim2  8461  uniqs  8757  xpassen  9045  dffi3  9379  dfsup2  9392  sup00  9413  r1limg  9731  jech9.3  9774  rankxplim2  9840  rankxplim3  9841  rankxpsuc  9842  dfac5lem2  10082  kmlem11  10119  cflim2  10222  fin23lem30  10301  fin23lem34  10305  itunisuc  10378  itunitc  10380  ituniiun  10381  ac6num  10438  rankcf  10737  dprd2da  20086  dmdprdsplit2lem  20089  lssuni  21008  basdif0  23015  tgdif0  23054  neiptopuni  23192  restcls  23243  restntr  23244  pnrmopn  23405  cncmp  23454  discmp  23460  hauscmplem  23468  unisngl  23589  xkouni  23661  uptx  23687  ufildr  23993  ptcmplem3  24116  utop2nei  24312  utopreg  24314  zcld  24876  icccmp  24888  cncfcnvcn  24989  cnmpopc  24992  cnheibor  25019  evth  25023  evth2  25024  iunmbl  25617  voliun  25618  dvcnvrelem2  26082  ftc1  26106  aannenlem2  26395  bday1  27909  old0  27934  made0  27958  old1  27960  madeoldsuc  27980  isconstr  34035  circtopn  34136  locfinref  34140  zarmxt1  34179  tpr2rico  34211  cbvesum  34341  cbvesumv  34342  unibrsiga  34485  sxbrsigalem3  34571  dya2iocucvr  34583  sxbrsigalem1  34584  sibf0  34633  sibff  34635  sitgclg  34641  probfinmeasbALTV  34728  coinflipuniv  34781  fineqvnttrclse  35424  wevgblacfn  35458  cvmliftlem10  35649  dfon2lem7  36142  dfrdg2  36148  dfiota3  36276  dffv5  36277  dfrecs2  36305  dfrdg4  36306  ordcmp  36812  ttcuni  36878  bj-nuliotaALT  37548  mptsnun  37838  finxp1o  37891  ftc1cnnc  38196  cnvepima  38841  sn-iotalemcor  42846  onsucunitp  43955  dfom6  44112  refsum2cnlem1  45622  lptre2pt  46219  limclner  46230  limclr  46234  stoweidlem62  46641  fourierdlem42  46728  fourierdlem80  46765  fouriercnp  46805  qndenserrn  46878  salexct3  46921  salgencntex  46922  salgensscntex  46923  subsalsal  46938  0ome  47108  borelmbl  47215  mbfresmf  47318  cnfsmf  47319  incsmf  47321  smfmbfcex  47339  decsmf  47346  smfpimbor1lem2  47378  dftpos5  49500  ipoglb0  49620  setrec2  50321