Theorem unieqi 4870

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

Syntax hints:   = wceq 1540  ∪ cuni 4858

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  elunirab  4873  unisng  4876  unidif0  5299  univ  5394  uniop  5458  dfiun3g  5909  op1sta  6174  op2nda  6177  dfdm2  6229  unixpid  6232  unisucs  6386  iotajust  6437  dfiota2  6439  cbviotaw  6445  cbviotavw  6446  cbviota  6447  sb8iota  6449  dffv4  6819  funfv2f  6912  funiunfv  7184  elunirnALT  7188  riotauni  7312  ordunisuc  7765  1st0  7930  2nd0  7931  unielxp  7962  brtpos0  8166  frrlem5  8223  frrlem8  8226  frrlem10  8228  dfrecs3  8295  recsfval  8303  tz7.44-3  8330  nlim1  8407  nlim2  8408  uniqs  8701  xpassen  8988  dffi3  9321  dfsup2  9334  sup00  9355  r1limg  9667  jech9.3  9710  rankxplim2  9776  rankxplim3  9777  rankxpsuc  9778  dfac5lem2  10018  kmlem11  10055  cflim2  10157  fin23lem30  10236  fin23lem34  10240  itunisuc  10313  itunitc  10315  ituniiun  10316  ac6num  10373  rankcf  10671  dprd2da  19923  dmdprdsplit2lem  19926  lssuni  20842  basdif0  22838  tgdif0  22877  neiptopuni  23015  restcls  23066  restntr  23067  pnrmopn  23228  cncmp  23277  discmp  23283  hauscmplem  23291  unisngl  23412  xkouni  23484  uptx  23510  ufildr  23816  ptcmplem3  23939  utop2nei  24136  utopreg  24138  zcld  24700  icccmp  24712  cncfcnvcn  24817  cnmpopc  24820  cnheibor  24852  evth  24856  evth2  24857  iunmbl  25452  voliun  25453  dvcnvrelem2  25921  ftc1  25947  aannenlem2  26235  bday1s  27746  old0  27771  made0  27789  old1  27791  madeoldsuc  27801  zs12bday  28365  isconstr  33719  circtopn  33820  locfinref  33824  zarmxt1  33863  tpr2rico  33895  cbvesum  34025  cbvesumv  34026  unibrsiga  34169  sxbrsigalem3  34256  dya2iocucvr  34268  sxbrsigalem1  34269  sibf0  34318  sibff  34320  sitgclg  34326  probfinmeasbALTV  34413  coinflipuniv  34466  fineqvnttrclse  35093  wevgblacfn  35102  cvmliftlem10  35287  dfon2lem7  35783  dfrdg2  35789  dfiota3  35917  dffv5  35918  dfrecs2  35944  dfrdg4  35945  ordcmp  36441  bj-nuliotaALT  37052  mptsnun  37333  finxp1o  37386  ftc1cnnc  37692  cnvepima  38325  sn-iotalemcor  42215  onsucunitp  43366  dfom6  43524  refsum2cnlem1  45035  lptre2pt  45641  limclner  45652  limclr  45656  stoweidlem62  46063  fourierdlem42  46150  fourierdlem80  46187  fouriercnp  46227  qndenserrn  46300  salexct3  46343  salgencntex  46344  salgensscntex  46345  subsalsal  46360  0ome  46530  borelmbl  46637  mbfresmf  46740  cnfsmf  46741  incsmf  46743  smfmbfcex  46761  decsmf  46768  smfpimbor1lem2  46800  dftpos5  48878  ipoglb0  48998  setrec2  49700