Theorem unieqi 4919

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

Syntax hints:   = wceq 1540  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  elunirab  4922  unisng  4925  unidif0  5360  univ  5456  uniop  5520  dfiun3g  5978  op1sta  6245  op2nda  6248  dfdm2  6301  unixpid  6304  unisucs  6461  iotajust  6513  dfiota2  6515  cbviotaw  6521  cbviotavw  6522  cbviota  6523  sb8iota  6525  dffv4  6903  funfv2f  6998  funiunfv  7268  elunirnALT  7272  riotauni  7394  ordunisuc  7852  1st0  8020  2nd0  8021  unielxp  8052  brtpos0  8258  frrlem5  8315  frrlem8  8318  frrlem10  8320  dfwrecsOLD  8338  dfrecs3  8412  dfrecs3OLD  8413  recsfval  8421  tz7.44-3  8448  nlim1  8527  nlim2  8528  uniqs  8817  xpassen  9106  dffi3  9471  dfsup2  9484  sup00  9504  r1limg  9811  jech9.3  9854  rankxplim2  9920  rankxplim3  9921  rankxpsuc  9922  dfac5lem2  10164  kmlem11  10201  cflim2  10303  fin23lem30  10382  fin23lem34  10386  itunisuc  10459  itunitc  10461  ituniiun  10462  ac6num  10519  rankcf  10817  dprd2da  20062  dmdprdsplit2lem  20065  lssuni  20937  basdif0  22960  tgdif0  22999  neiptopuni  23138  restcls  23189  restntr  23190  pnrmopn  23351  cncmp  23400  discmp  23406  hauscmplem  23414  unisngl  23535  xkouni  23607  uptx  23633  ufildr  23939  ptcmplem3  24062  utop2nei  24259  utopreg  24261  zcld  24835  icccmp  24847  cncfcnvcn  24952  cnmpopc  24955  cnheibor  24987  evth  24991  evth2  24992  iunmbl  25588  voliun  25589  dvcnvrelem2  26057  ftc1  26083  aannenlem2  26371  bday1s  27876  old0  27898  made0  27912  old1  27914  madeoldsuc  27923  zs12bday  28424  isconstr  33777  circtopn  33836  locfinref  33840  zarmxt1  33879  tpr2rico  33911  cbvesum  34043  cbvesumv  34044  unibrsiga  34187  sxbrsigalem3  34274  dya2iocucvr  34286  sxbrsigalem1  34287  sibf0  34336  sibff  34338  sitgclg  34344  probfinmeasbALTV  34431  coinflipuniv  34484  wevgblacfn  35114  cvmliftlem10  35299  dfon2lem7  35790  dfrdg2  35796  dfiota3  35924  dffv5  35925  dfrecs2  35951  dfrdg4  35952  ordcmp  36448  bj-nuliotaALT  37059  mptsnun  37340  finxp1o  37393  ftc1cnnc  37699  uniqsALTV  38330  cnvepima  38338  sn-iotalemcor  42261  onsucunitp  43386  dfom6  43544  refsum2cnlem1  45042  lptre2pt  45655  limclner  45666  limclr  45670  stoweidlem62  46077  fourierdlem42  46164  fourierdlem80  46201  fouriercnp  46241  qndenserrn  46314  salexct3  46357  salgencntex  46358  salgensscntex  46359  subsalsal  46374  0ome  46544  borelmbl  46651  mbfresmf  46754  cnfsmf  46755  incsmf  46757  smfmbfcex  46775  decsmf  46782  smfpimbor1lem2  46814  dftpos5  48774  ipoglb0  48883  setrec2  49214