Theorem unieqi 4921

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

Syntax hints:   = wceq 1541  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909

This theorem is referenced by:  elunirab  4924  unisng  4929  unidif0  5358  univ  5451  uniop  5515  dfiun3g  5963  op1sta  6224  op2nda  6227  dfdm2  6280  unixpid  6283  unisucs  6441  iotajust  6494  dfiota2  6496  cbviotaw  6502  cbviotavw  6503  cbviota  6505  sb8iota  6507  dffv4  6888  funfv2f  6980  funiunfv  7249  elunirnALT  7253  riotauni  7373  ordunisuc  7822  1st0  7983  2nd0  7984  unielxp  8015  brtpos0  8220  frrlem5  8277  frrlem8  8280  frrlem10  8282  dfwrecsOLD  8300  dfrecs3  8374  dfrecs3OLD  8375  recsfval  8383  tz7.44-3  8410  nlim1  8491  nlim2  8492  uniqs  8773  xpassen  9068  dffi3  9428  dfsup2  9441  sup00  9461  r1limg  9768  jech9.3  9811  rankxplim2  9877  rankxplim3  9878  rankxpsuc  9879  dfac5lem2  10121  kmlem11  10157  cflim2  10260  fin23lem30  10339  fin23lem34  10343  itunisuc  10416  itunitc  10418  ituniiun  10419  ac6num  10476  rankcf  10774  dprd2da  19953  dmdprdsplit2lem  19956  lssuni  20694  basdif0  22676  tgdif0  22715  neiptopuni  22854  restcls  22905  restntr  22906  pnrmopn  23067  cncmp  23116  discmp  23122  hauscmplem  23130  unisngl  23251  xkouni  23323  uptx  23349  ufildr  23655  ptcmplem3  23778  utop2nei  23975  utopreg  23977  zcld  24549  icccmp  24561  cncfcnvcn  24665  cnmpopc  24668  cnheibor  24695  evth  24699  evth2  24700  iunmbl  25294  voliun  25295  dvcnvrelem2  25759  ftc1  25783  aannenlem2  26066  bday1s  27557  old0  27579  made0  27593  old1  27595  madeoldsuc  27604  circtopn  33103  locfinref  33107  zarmxt1  33146  tpr2rico  33178  cbvesum  33326  unibrsiga  33470  sxbrsigalem3  33557  dya2iocucvr  33569  sxbrsigalem1  33570  sibf0  33619  sibff  33621  sitgclg  33627  probfinmeasbALTV  33714  coinflipuniv  33766  cvmliftlem10  34571  dfon2lem7  35053  dfrdg2  35059  dfiota3  35187  dffv5  35188  dfrecs2  35214  dfrdg4  35215  ordcmp  35635  bj-nuliotaALT  36242  mptsnun  36523  finxp1o  36576  ftc1cnnc  36863  uniqsALTV  37501  cnvepima  37509  sn-iotalemcor  41345  onsucunitp  42425  dfom6  42584  refsum2cnlem1  44023  lptre2pt  44655  limclner  44666  limclr  44670  stoweidlem62  45077  fourierdlem42  45164  fourierdlem80  45201  fouriercnp  45241  qndenserrn  45314  salexct3  45357  salgencntex  45358  salgensscntex  45359  subsalsal  45374  0ome  45544  borelmbl  45651  mbfresmf  45754  cnfsmf  45755  incsmf  45757  smfmbfcex  45775  decsmf  45782  smfpimbor1lem2  45814  ipoglb0  47707  setrec2  47828