Theorem unieqi 4806

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

Syntax hints:   = wceq 1542  ∪ cuni 4793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-uni 4794

This theorem is referenced by:  elunirab  4809  unisng  4814  unidif0  5223  univ  5307  uniop  5369  dfiun3g  5801  op1sta  6051  op2nda  6054  dfdm2  6107  unixpid  6110  unisuc  6242  iotajust  6290  dfiota2  6292  cbviotaw  6298  cbviotavw  6299  cbviota  6301  sb8iota  6303  dffv4  6665  funfv2f  6751  funiunfv  7012  elunirnALT  7016  riotauni  7127  ordunisuc  7560  1st0  7713  2nd0  7714  unielxp  7745  brtpos0  7921  dfrecs3  8031  recsfval  8039  tz7.44-3  8066  uniqs  8381  xpassen  8653  dffi3  8961  dfsup2  8974  sup00  8994  r1limg  9266  jech9.3  9309  rankxplim2  9375  rankxplim3  9376  rankxpsuc  9377  dfac5lem2  9617  kmlem11  9653  cflim2  9756  fin23lem30  9835  fin23lem34  9839  itunisuc  9912  itunitc  9914  ituniiun  9915  ac6num  9972  rankcf  10270  dprd2da  19276  dmdprdsplit2lem  19279  lssuni  19823  basdif0  21697  tgdif0  21736  neiptopuni  21874  restcls  21925  restntr  21926  pnrmopn  22087  cncmp  22136  discmp  22142  hauscmplem  22150  unisngl  22271  xkouni  22343  uptx  22369  ufildr  22675  ptcmplem3  22798  utop2nei  22995  utopreg  22997  zcld  23558  icccmp  23570  cncfcnvcn  23670  cnmpopc  23673  cnheibor  23700  evth  23704  evth2  23705  iunmbl  24298  voliun  24299  dvcnvrelem2  24762  ftc1  24786  aannenlem2  25069  circtopn  31351  locfinref  31355  zarmxt1  31394  tpr2rico  31426  cbvesum  31572  unibrsiga  31716  sxbrsigalem3  31801  dya2iocucvr  31813  sxbrsigalem1  31814  sibf0  31863  sibff  31865  sitgclg  31871  probfinmeasbALTV  31958  coinflipuniv  32010  cvmliftlem10  32819  dfon2lem7  33329  dfrdg2  33335  frrlem5  33437  frrlem8  33440  frrlem10  33442  bday1s  33658  old0  33686  made0  33687  madeoldsuc  33697  dfiota3  33855  dffv5  33856  dfrecs2  33882  dfrdg4  33883  ordcmp  34266  bj-nuliotaALT  34841  mptsnun  35122  finxp1o  35175  ftc1cnnc  35461  uniqsALTV  36076  cnvepima  36084  dfom6  40676  refsum2cnlem1  42102  lptre2pt  42707  limclner  42718  limclr  42722  stoweidlem62  43129  fourierdlem42  43216  fourierdlem80  43253  fouriercnp  43293  qndenserrn  43366  salexct3  43407  salgencntex  43408  salgensscntex  43409  subsalsal  43424  0ome  43593  borelmbl  43700  mbfresmf  43798  cnfsmf  43799  incsmf  43801  smfmbfcex  43818  decsmf  43825  smfpimbor1lem2  43856  setrec2  45838