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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  elunirab  4885  unisng  4888  unidif0  5325  unidif0OLD  5326  univ  5423  uniop  5492  dfiun3g  5956  op1sta  6238  op2nda  6241  dfdm2  6299  unixpid  6302  unisucs  6457  iotajust  6508  dfiota2  6510  cbviotaw  6516  cbviotavw  6517  cbviota  6518  sb8iota  6520  dffv4  6902  funfv2f  6994  funiunfv  7272  elunirnALT  7276  riotauni  7403  ordunisuc  7864  1st0  8028  2nd0  8029  unielxp  8060  brtpos0  8275  frrlem5  8333  frrlem8  8336  frrlem10  8338  dfrecs3  8405  recsfval  8413  tz7.44-3  8441  nlim1  8522  nlim2  8523  uniqs  8819  xpassen  9115  dffi3  9447  dfsup2  9460  sup00  9481  r1limg  9802  jech9.3OLD  9847  rankxplim2  9921  rankxplim3  9922  rankxpsuc  9923  setrec2  10001  dfac5lem2  10227  kmlem11  10263  fin23lem30  10444  fin23lem34  10448  itunisuc  10521  itunitc  10523  ituniiun  10524  ac6num  10581  rankcf  10886  dprd2da  20285  dmdprdsplit2lem  20288  lssuni  21241  basdif0  23298  tgdif0  23337  neiptopuni  23475  restcls  23526  restntr  23527  pnrmopn  23688  cncmp  23737  discmp  23743  hauscmplem  23751  unisngl  23873  xkouni  23945  uptx  23971  ufildr  24277  ptcmplem3  24400  utop2nei  24596  utopreg  24598  zcld  25160  icccmp  25172  cncfcnvcn  25273  cnmpopc  25276  cnheibor  25303  evth  25307  evth2  25308  iunmbl  25901  voliun  25902  dvcnvrelem2  26365  ftc1  26389  aannenlem2  26683  bday1  28227  old0  28252  made0  28276  old1  28278  madeoldsuc  28298  isconstr  34435  circtopn  34536  locfinref  34540  zarmxt1  34579  tpr2rico  34611  cbvesum  34741  cbvesumv  34742  unibrsiga  34886  sxbrsigalem3  34971  dya2iocucvr  34983  sxbrsigalem1  34984  sibf0  35033  sibff  35035  sitgclg  35041  probfinmeasbALTV  35128  coinflipuniv  35181  fineqvnttrclse  35891  wevgblacfn  36038  cvmliftlem10  36225  dfon2lem7  36728  dfrdg2  36734  dfiota3  36862  dffv5  36863  dfrecs2  36891  dfrdg4  36892  ordcmp  37412  ttcuni  37478  bj-nuliotaALT  38163  mptsnun  38453  finxp1o  38506  ftc1cnnc  38801  cnvepima  39460  sn-iotalemcor  43467  onsucunitp  44565  dfom6  44722  refsum2cnlem1  46257  lptre2pt  46853  limclner  46864  limclr  46868  stoweidlem62  47275  fourierdlem42  47362  fourierdlem80  47399  fouriercnp  47439  qndenserrn  47512  salexct3  47555  salgencntex  47556  salgensscntex  47557  subsalsal  47572  0ome  47742  borelmbl  47849  mbfresmf  47952  cnfsmf  47953  incsmf  47955  smfmbfcex  47973  decsmf  47980  smfpimbor1lem2  48012  dftpos5  50190  ipoglb0  50311