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 1542  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  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  5962  op1sta  6222  op2nda  6225  dfdm2  6278  unixpid  6281  unisucs  6439  iotajust  6492  dfiota2  6494  cbviotaw  6500  cbviotavw  6501  cbviota  6503  sb8iota  6505  dffv4  6886  funfv2f  6978  funiunfv  7244  elunirnALT  7248  riotauni  7368  ordunisuc  7817  1st0  7978  2nd0  7979  unielxp  8010  brtpos0  8215  frrlem5  8272  frrlem8  8275  frrlem10  8277  dfwrecsOLD  8295  dfrecs3  8369  dfrecs3OLD  8370  recsfval  8378  tz7.44-3  8405  nlim1  8486  nlim2  8487  uniqs  8768  xpassen  9063  dffi3  9423  dfsup2  9436  sup00  9456  r1limg  9763  jech9.3  9806  rankxplim2  9872  rankxplim3  9873  rankxpsuc  9874  dfac5lem2  10116  kmlem11  10152  cflim2  10255  fin23lem30  10334  fin23lem34  10338  itunisuc  10411  itunitc  10413  ituniiun  10414  ac6num  10471  rankcf  10769  dprd2da  19907  dmdprdsplit2lem  19910  lssuni  20543  basdif0  22448  tgdif0  22487  neiptopuni  22626  restcls  22677  restntr  22678  pnrmopn  22839  cncmp  22888  discmp  22894  hauscmplem  22902  unisngl  23023  xkouni  23095  uptx  23121  ufildr  23427  ptcmplem3  23550  utop2nei  23747  utopreg  23749  zcld  24321  icccmp  24333  cncfcnvcn  24433  cnmpopc  24436  cnheibor  24463  evth  24467  evth2  24468  iunmbl  25062  voliun  25063  dvcnvrelem2  25527  ftc1  25551  aannenlem2  25834  bday1s  27322  old0  27344  made0  27358  old1  27360  madeoldsuc  27369  circtopn  32806  locfinref  32810  zarmxt1  32849  tpr2rico  32881  cbvesum  33029  unibrsiga  33173  sxbrsigalem3  33260  dya2iocucvr  33272  sxbrsigalem1  33273  sibf0  33322  sibff  33324  sitgclg  33330  probfinmeasbALTV  33417  coinflipuniv  33469  cvmliftlem10  34274  dfon2lem7  34750  dfrdg2  34756  dfiota3  34884  dffv5  34885  dfrecs2  34911  dfrdg4  34912  ordcmp  35321  bj-nuliotaALT  35928  mptsnun  36209  finxp1o  36262  ftc1cnnc  36549  uniqsALTV  37187  cnvepima  37195  sn-iotalemcor  41036  onsucunitp  42109  dfom6  42268  refsum2cnlem1  43707  lptre2pt  44343  limclner  44354  limclr  44358  stoweidlem62  44765  fourierdlem42  44852  fourierdlem80  44889  fouriercnp  44929  qndenserrn  45002  salexct3  45045  salgencntex  45046  salgensscntex  45047  subsalsal  45062  0ome  45232  borelmbl  45339  mbfresmf  45442  cnfsmf  45443  incsmf  45445  smfmbfcex  45463  decsmf  45470  smfpimbor1lem2  45502  ipoglb0  47573  setrec2  47694