Theorem unieqi 4883

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

Syntax hints:   = wceq 1540  ∪ cuni 4871

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 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  elunirab  4886  unisng  4889  unidif0  5315  univ  5411  uniop  5475  dfiun3g  5931  op1sta  6198  op2nda  6201  dfdm2  6254  unixpid  6257  unisucs  6411  iotajust  6463  dfiota2  6465  cbviotaw  6471  cbviotavw  6472  cbviota  6473  sb8iota  6475  dffv4  6855  funfv2f  6950  funiunfv  7222  elunirnALT  7226  riotauni  7350  ordunisuc  7807  1st0  7974  2nd0  7975  unielxp  8006  brtpos0  8212  frrlem5  8269  frrlem8  8272  frrlem10  8274  dfrecs3  8341  recsfval  8349  tz7.44-3  8376  nlim1  8453  nlim2  8454  uniqs  8747  xpassen  9035  dffi3  9382  dfsup2  9395  sup00  9416  r1limg  9724  jech9.3  9767  rankxplim2  9833  rankxplim3  9834  rankxpsuc  9835  dfac5lem2  10077  kmlem11  10114  cflim2  10216  fin23lem30  10295  fin23lem34  10299  itunisuc  10372  itunitc  10374  ituniiun  10375  ac6num  10432  rankcf  10730  dprd2da  19974  dmdprdsplit2lem  19977  lssuni  20845  basdif0  22840  tgdif0  22879  neiptopuni  23017  restcls  23068  restntr  23069  pnrmopn  23230  cncmp  23279  discmp  23285  hauscmplem  23293  unisngl  23414  xkouni  23486  uptx  23512  ufildr  23818  ptcmplem3  23941  utop2nei  24138  utopreg  24140  zcld  24702  icccmp  24714  cncfcnvcn  24819  cnmpopc  24822  cnheibor  24854  evth  24858  evth2  24859  iunmbl  25454  voliun  25455  dvcnvrelem2  25923  ftc1  25949  aannenlem2  26237  bday1s  27743  old0  27767  made0  27785  old1  27787  madeoldsuc  27796  zs12bday  28343  isconstr  33726  circtopn  33827  locfinref  33831  zarmxt1  33870  tpr2rico  33902  cbvesum  34032  cbvesumv  34033  unibrsiga  34176  sxbrsigalem3  34263  dya2iocucvr  34275  sxbrsigalem1  34276  sibf0  34325  sibff  34327  sitgclg  34333  probfinmeasbALTV  34420  coinflipuniv  34473  wevgblacfn  35096  cvmliftlem10  35281  dfon2lem7  35777  dfrdg2  35783  dfiota3  35911  dffv5  35912  dfrecs2  35938  dfrdg4  35939  ordcmp  36435  bj-nuliotaALT  37046  mptsnun  37327  finxp1o  37380  ftc1cnnc  37686  cnvepima  38319  sn-iotalemcor  42210  onsucunitp  43362  dfom6  43520  refsum2cnlem1  45031  lptre2pt  45638  limclner  45649  limclr  45653  stoweidlem62  46060  fourierdlem42  46147  fourierdlem80  46184  fouriercnp  46224  qndenserrn  46297  salexct3  46340  salgencntex  46341  salgensscntex  46342  subsalsal  46357  0ome  46527  borelmbl  46634  mbfresmf  46737  cnfsmf  46738  incsmf  46740  smfmbfcex  46758  decsmf  46765  smfpimbor1lem2  46797  dftpos5  48862  ipoglb0  48982  setrec2  49684