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 ⊢ ∪ 𝐴 = ∪ 𝐵

This proof depends on syntax axioms:   = wceq 1569  ∪ cuni 4871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872

This theorem is used by:  elunirab  4886  unisng  4889  unidif0  5329  unidif0OLD  5330  univ  5431  uniop  5497  dfiun3g  5957  op1sta  6225  op2nda  6228  dfdm2  6282  unixpid  6285  unisucs  6440  iotajust  6491  dfiota2  6493  cbviotaw  6499  cbviotavw  6500  cbviota  6501  sb8iota  6503  dffv4  6878  funfv2f  6970  funiunfv  7246  elunirnALT  7250  riotauni  7375  ordunisuc  7826  1st0  7990  2nd0  7991  unielxp  8022  brtpos0  8227  frrlem5  8285  frrlem8  8288  frrlem10  8290  dfrecs3  8357  recsfval  8365  tz7.44-3  8393  nlim1  8472  nlim2  8473  uniqs  8769  xpassen  9057  dffi3  9389  dfsup2  9402  sup00  9423  r1limg  9741  jech9.3  9784  rankxplim2  9850  rankxplim3  9851  rankxpsuc  9852  dfac5lem2  10115  kmlem11  10151  cflim2  10253  fin23lem30  10332  fin23lem34  10336  itunisuc  10409  itunitc  10411  ituniiun  10412  ac6num  10469  rankcf  10768  dprd2da  20120  dmdprdsplit2lem  20123  lssuni  21071  basdif0  23121  tgdif0  23160  neiptopuni  23298  restcls  23349  restntr  23350  pnrmopn  23511  cncmp  23560  discmp  23566  hauscmplem  23574  unisngl  23695  xkouni  23767  uptx  23793  ufildr  24099  ptcmplem3  24222  utop2nei  24418  utopreg  24420  zcld  24982  icccmp  24994  cncfcnvcn  25095  cnmpopc  25098  cnheibor  25125  evth  25129  evth2  25130  iunmbl  25723  voliun  25724  dvcnvrelem2  26188  ftc1  26212  aannenlem2  26503  bday1  28018  old0  28043  made0  28067  old1  28069  madeoldsuc  28089  isconstr  34135  circtopn  34236  locfinref  34240  zarmxt1  34279  tpr2rico  34311  cbvesum  34441  cbvesumv  34442  unibrsiga  34585  sxbrsigalem3  34671  dya2iocucvr  34683  sxbrsigalem1  34684  sibf0  34733  sibff  34735  sitgclg  34741  probfinmeasbALTV  34828  coinflipuniv  34881  fineqvnttrclse  35545  wevgblacfn  35603  cvmliftlem10  35794  dfon2lem7  36287  dfrdg2  36293  dfiota3  36421  dffv5  36422  dfrecs2  36450  dfrdg4  36451  ordcmp  36986  ttcuni  37052  bj-nuliotaALT  37722  mptsnun  38013  finxp1o  38066  ftc1cnnc  38371  cnvepima  39014  sn-iotalemcor  43021  onsucunitp  44128  dfom6  44285  refsum2cnlem1  45785  lptre2pt  46382  limclner  46393  limclr  46397  stoweidlem62  46804  fourierdlem42  46891  fourierdlem80  46928  fouriercnp  46968  qndenserrn  47041  salexct3  47084  salgencntex  47085  salgensscntex  47086  subsalsal  47101  0ome  47271  borelmbl  47378  mbfresmf  47481  cnfsmf  47482  incsmf  47484  smfmbfcex  47502  decsmf  47509  smfpimbor1lem2  47541  dftpos5  49680  ipoglb0  49800  setrec2  50501