Theorem unieqi 4381

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

Syntax hints:   = wceq 1475  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373

This theorem is referenced by:  elunirab  4384  unisn  4387  unidif0  4764  univ  4846  uniop  4902  dfiun3g  5299  op1sta  5535  op2nda  5538  dfdm2  5584  unixpid  5587  unisuc  5718  iotajust  5767  dfiota2  5769  cbviota  5773  sb8iota  5775  dffv4  6100  funfv2f  6177  funiunfv  6410  elunirnALT  6414  riotauni  6517  ordunisuc  6924  1st0  7065  2nd0  7066  unielxp  7095  brtpos0  7246  dfrecs3  7356  recsfval  7364  tz7.44-3  7391  uniqs  7694  xpassen  7939  dffi3  8220  dfsup2  8233  sup00  8253  r1limg  8517  jech9.3  8560  rankxplim2  8626  rankxplim3  8627  rankxpsuc  8628  dfac5lem2  8830  kmlem11  8865  cflim2  8968  fin23lem30  9047  fin23lem34  9051  itunisuc  9124  itunitc  9126  ituniiun  9127  ac6num  9184  rankcf  9478  dprd2da  18264  dmdprdsplit2lem  18267  lssuni  18761  basdif0  20568  tgdif0  20607  neiptopuni  20744  restcls  20795  restntr  20796  pnrmopn  20957  cncmp  21005  discmp  21011  hauscmplem  21019  unisngl  21140  xkouni  21212  uptx  21238  ufildr  21545  ptcmplem3  21668  utop2nei  21864  utopreg  21866  zcld  22424  icccmp  22436  cncfcnvcn  22532  cnmpt2pc  22535  cnheibor  22562  evth  22566  evth2  22567  iunmbl  23128  voliun  23129  dvcnvrelem2  23585  ftc1  23609  aannenlem2  23888  circtopn  29232  locfinref  29236  tpr2rico  29286  cbvesum  29431  unibrsiga  29576  sxbrsigalem3  29661  dya2iocucvr  29673  sxbrsigalem1  29674  sibf0  29723  sibff  29725  sitgclg  29731  probfinmeasbOLD  29817  coinflipuniv  29870  cvmliftlem10  30530  dfon2lem7  30938  dfrdg2  30945  frrlem11  31036  dfiota3  31200  dffv5  31201  dfrecs2  31227  dfrdg4  31228  ordcmp  31616  bj-nuliotaALT  32211  mptsnun  32362  finxp1o  32405  ftc1cnnc  32654  refsum2cnlem1  38219  lptre2pt  38707  limclner  38718  limclr  38722  stoweidlem62  38955  fourierdlem42  39042  fourierdlem80  39079  fouriercnp  39119  qndenserrn  39195  salexct3  39236  salgencntex  39237  salgensscntex  39238  subsalsal  39253  0ome  39419  borelmbl  39526  mbfresmf  39626  cnfsmf  39627  incsmf  39629  smfmbfcex  39646  decsmf  39653  smfpimbor1lem2  39684  setrec2  42241