Theorem unieqi 4882

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

This proof depends on syntax axioms:   = wceq 1570  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  elunirab  4885  unisng  4888  unidif0  5328  unidif0OLD  5329  univ  5430  uniop  5496  dfiun3g  5956  op1sta  6225  op2nda  6228  dfdm2  6283  unixpid  6286  unisucs  6441  iotajust  6492  dfiota2  6494  cbviotaw  6500  cbviotavw  6501  cbviota  6502  sb8iota  6504  dffv4  6879  funfv2f  6971  funiunfv  7248  elunirnALT  7252  riotauni  7379  ordunisuc  7831  1st0  7995  2nd0  7996  unielxp  8027  brtpos0  8234  frrlem5  8292  frrlem8  8295  frrlem10  8297  dfrecs3  8364  recsfval  8372  tz7.44-3  8400  nlim1  8479  nlim2  8480  uniqs  8776  xpassen  9072  dffi3  9404  dfsup2  9417  sup00  9438  r1limg  9756  jech9.3  9799  rankxplim2  9865  rankxplim3  9866  rankxpsuc  9867  dfac5lem2  10130  kmlem11  10166  cflim2  10268  fin23lem30  10347  fin23lem34  10351  itunisuc  10424  itunitc  10426  ituniiun  10427  ac6num  10484  rankcf  10789  dprd2da  20172  dmdprdsplit2lem  20175  lssuni  21124  basdif0  23179  tgdif0  23218  neiptopuni  23356  restcls  23407  restntr  23408  pnrmopn  23569  cncmp  23618  discmp  23624  hauscmplem  23632  unisngl  23754  xkouni  23826  uptx  23852  ufildr  24158  ptcmplem3  24281  utop2nei  24477  utopreg  24479  zcld  25041  icccmp  25053  cncfcnvcn  25154  cnmpopc  25157  cnheibor  25184  evth  25188  evth2  25189  iunmbl  25782  voliun  25783  dvcnvrelem2  26247  ftc1  26271  aannenlem2  26562  bday1  28077  old0  28102  made0  28126  old1  28128  madeoldsuc  28148  isconstr  34233  circtopn  34334  locfinref  34338  zarmxt1  34377  tpr2rico  34409  cbvesum  34539  cbvesumv  34540  unibrsiga  34684  sxbrsigalem3  34770  dya2iocucvr  34782  sxbrsigalem1  34783  sibf0  34832  sibff  34834  sitgclg  34840  probfinmeasbALTV  34927  coinflipuniv  34980  fineqvnttrclse  35637  wevgblacfn  35695  cvmliftlem10  35860  dfon2lem7  36353  dfrdg2  36359  dfiota3  36487  dffv5  36488  dfrecs2  36516  dfrdg4  36517  ordcmp  37053  ttcuni  37119  bj-nuliotaALT  37789  mptsnun  38080  finxp1o  38133  ftc1cnnc  38428  cnvepima  39072  sn-iotalemcor  43079  onsucunitp  44201  dfom6  44358  refsum2cnlem1  45858  lptre2pt  46455  limclner  46466  limclr  46470  stoweidlem62  46877  fourierdlem42  46964  fourierdlem80  47001  fouriercnp  47041  qndenserrn  47114  salexct3  47157  salgencntex  47158  salgensscntex  47159  subsalsal  47174  0ome  47344  borelmbl  47451  mbfresmf  47554  cnfsmf  47555  incsmf  47557  smfmbfcex  47575  decsmf  47582  smfpimbor1lem2  47614  dftpos5  49787  ipoglb0  49907  setrec2  50608