Theorem unieqi 4943

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

Syntax hints:   = wceq 1537  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  elunirab  4946  unisng  4949  unidif0  5378  univ  5471  uniop  5534  dfiun3g  5990  op1sta  6256  op2nda  6259  dfdm2  6312  unixpid  6315  unisucs  6472  iotajust  6524  dfiota2  6526  cbviotaw  6532  cbviotavw  6533  cbviota  6535  sb8iota  6537  dffv4  6917  funfv2f  7011  funiunfv  7285  elunirnALT  7289  riotauni  7410  ordunisuc  7868  1st0  8036  2nd0  8037  unielxp  8068  brtpos0  8274  frrlem5  8331  frrlem8  8334  frrlem10  8336  dfwrecsOLD  8354  dfrecs3  8428  dfrecs3OLD  8429  recsfval  8437  tz7.44-3  8464  nlim1  8545  nlim2  8546  uniqs  8835  xpassen  9132  dffi3  9500  dfsup2  9513  sup00  9533  r1limg  9840  jech9.3  9883  rankxplim2  9949  rankxplim3  9950  rankxpsuc  9951  dfac5lem2  10193  kmlem11  10230  cflim2  10332  fin23lem30  10411  fin23lem34  10415  itunisuc  10488  itunitc  10490  ituniiun  10491  ac6num  10548  rankcf  10846  dprd2da  20086  dmdprdsplit2lem  20089  lssuni  20960  basdif0  22981  tgdif0  23020  neiptopuni  23159  restcls  23210  restntr  23211  pnrmopn  23372  cncmp  23421  discmp  23427  hauscmplem  23435  unisngl  23556  xkouni  23628  uptx  23654  ufildr  23960  ptcmplem3  24083  utop2nei  24280  utopreg  24282  zcld  24854  icccmp  24866  cncfcnvcn  24971  cnmpopc  24974  cnheibor  25006  evth  25010  evth2  25011  iunmbl  25607  voliun  25608  dvcnvrelem2  26077  ftc1  26103  aannenlem2  26389  bday1s  27894  old0  27916  made0  27930  old1  27932  madeoldsuc  27941  zs12bday  28442  circtopn  33783  locfinref  33787  zarmxt1  33826  tpr2rico  33858  cbvesum  34006  cbvesumv  34007  unibrsiga  34150  sxbrsigalem3  34237  dya2iocucvr  34249  sxbrsigalem1  34250  sibf0  34299  sibff  34301  sitgclg  34307  probfinmeasbALTV  34394  coinflipuniv  34446  wevgblacfn  35076  cvmliftlem10  35262  dfon2lem7  35753  dfrdg2  35759  dfiota3  35887  dffv5  35888  dfrecs2  35914  dfrdg4  35915  ordcmp  36413  bj-nuliotaALT  37024  mptsnun  37305  finxp1o  37358  ftc1cnnc  37652  uniqsALTV  38285  cnvepima  38293  sn-iotalemcor  42215  onsucunitp  43335  dfom6  43493  refsum2cnlem1  44937  lptre2pt  45561  limclner  45572  limclr  45576  stoweidlem62  45983  fourierdlem42  46070  fourierdlem80  46107  fouriercnp  46147  qndenserrn  46220  salexct3  46263  salgencntex  46264  salgensscntex  46265  subsalsal  46280  0ome  46450  borelmbl  46557  mbfresmf  46660  cnfsmf  46661  incsmf  46663  smfmbfcex  46681  decsmf  46688  smfpimbor1lem2  46720  ipoglb0  48666  setrec2  48787