Theorem unieqi 4895

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

Syntax hints:   = wceq 1540  ∪ cuni 4883

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  elunirab  4898  unisng  4901  unidif0  5330  univ  5426  uniop  5490  dfiun3g  5947  op1sta  6214  op2nda  6217  dfdm2  6270  unixpid  6273  unisucs  6430  iotajust  6482  dfiota2  6484  cbviotaw  6490  cbviotavw  6491  cbviota  6492  sb8iota  6494  dffv4  6872  funfv2f  6967  funiunfv  7239  elunirnALT  7243  riotauni  7366  ordunisuc  7824  1st0  7992  2nd0  7993  unielxp  8024  brtpos0  8230  frrlem5  8287  frrlem8  8290  frrlem10  8292  dfwrecsOLD  8310  dfrecs3  8384  dfrecs3OLD  8385  recsfval  8393  tz7.44-3  8420  nlim1  8499  nlim2  8500  uniqs  8789  xpassen  9078  dffi3  9441  dfsup2  9454  sup00  9475  r1limg  9783  jech9.3  9826  rankxplim2  9892  rankxplim3  9893  rankxpsuc  9894  dfac5lem2  10136  kmlem11  10173  cflim2  10275  fin23lem30  10354  fin23lem34  10358  itunisuc  10431  itunitc  10433  ituniiun  10434  ac6num  10491  rankcf  10789  dprd2da  20023  dmdprdsplit2lem  20026  lssuni  20894  basdif0  22889  tgdif0  22928  neiptopuni  23066  restcls  23117  restntr  23118  pnrmopn  23279  cncmp  23328  discmp  23334  hauscmplem  23342  unisngl  23463  xkouni  23535  uptx  23561  ufildr  23867  ptcmplem3  23990  utop2nei  24187  utopreg  24189  zcld  24751  icccmp  24763  cncfcnvcn  24868  cnmpopc  24871  cnheibor  24903  evth  24907  evth2  24908  iunmbl  25504  voliun  25505  dvcnvrelem2  25973  ftc1  25999  aannenlem2  26287  bday1s  27793  old0  27815  made0  27829  old1  27831  madeoldsuc  27840  zs12bday  28341  isconstr  33716  circtopn  33814  locfinref  33818  zarmxt1  33857  tpr2rico  33889  cbvesum  34019  cbvesumv  34020  unibrsiga  34163  sxbrsigalem3  34250  dya2iocucvr  34262  sxbrsigalem1  34263  sibf0  34312  sibff  34314  sitgclg  34320  probfinmeasbALTV  34407  coinflipuniv  34460  wevgblacfn  35077  cvmliftlem10  35262  dfon2lem7  35753  dfrdg2  35759  dfiota3  35887  dffv5  35888  dfrecs2  35914  dfrdg4  35915  ordcmp  36411  bj-nuliotaALT  37022  mptsnun  37303  finxp1o  37356  ftc1cnnc  37662  uniqsALTV  38293  cnvepima  38301  sn-iotalemcor  42219  onsucunitp  43344  dfom6  43502  refsum2cnlem1  45009  lptre2pt  45617  limclner  45628  limclr  45632  stoweidlem62  46039  fourierdlem42  46126  fourierdlem80  46163  fouriercnp  46203  qndenserrn  46276  salexct3  46319  salgencntex  46320  salgensscntex  46321  subsalsal  46336  0ome  46506  borelmbl  46613  mbfresmf  46716  cnfsmf  46717  incsmf  46719  smfmbfcex  46737  decsmf  46744  smfpimbor1lem2  46776  dftpos5  48797  ipoglb0  48916  setrec2  49507