Theorem unieqi 4813

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

Syntax hints:   = wceq 1538  ∪ cuni 4800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  elunirab  4816  unisng  4819  unidif0  5225  univ  5309  uniop  5370  dfiun3g  5800  op1sta  6049  op2nda  6052  dfdm2  6100  unixpid  6103  unisuc  6235  iotajust  6282  dfiota2  6284  cbviotaw  6290  cbviota  6292  sb8iota  6294  dffv4  6642  funfv2f  6727  funiunfv  6985  elunirnALT  6989  riotauni  7099  ordunisuc  7527  1st0  7677  2nd0  7678  unielxp  7709  brtpos0  7882  dfrecs3  7992  recsfval  8000  tz7.44-3  8027  uniqs  8340  xpassen  8594  dffi3  8879  dfsup2  8892  sup00  8912  r1limg  9184  jech9.3  9227  rankxplim2  9293  rankxplim3  9294  rankxpsuc  9295  dfac5lem2  9535  kmlem11  9571  cflim2  9674  fin23lem30  9753  fin23lem34  9757  itunisuc  9830  itunitc  9832  ituniiun  9833  ac6num  9890  rankcf  10188  dprd2da  19157  dmdprdsplit2lem  19160  lssuni  19704  basdif0  21558  tgdif0  21597  neiptopuni  21735  restcls  21786  restntr  21787  pnrmopn  21948  cncmp  21997  discmp  22003  hauscmplem  22011  unisngl  22132  xkouni  22204  uptx  22230  ufildr  22536  ptcmplem3  22659  utop2nei  22856  utopreg  22858  zcld  23418  icccmp  23430  cncfcnvcn  23530  cnmpopc  23533  cnheibor  23560  evth  23564  evth2  23565  iunmbl  24157  voliun  24158  dvcnvrelem2  24621  ftc1  24645  aannenlem2  24925  circtopn  31190  locfinref  31194  zarmxt1  31233  tpr2rico  31265  cbvesum  31411  unibrsiga  31555  sxbrsigalem3  31640  dya2iocucvr  31652  sxbrsigalem1  31653  sibf0  31702  sibff  31704  sitgclg  31710  probfinmeasbALTV  31797  coinflipuniv  31849  cvmliftlem10  32654  dfon2lem7  33147  dfrdg2  33153  frrlem5  33240  frrlem8  33243  frrlem10  33245  noetalem4  33333  dfiota3  33497  dffv5  33498  dfrecs2  33524  dfrdg4  33525  ordcmp  33908  bj-nuliotaALT  34475  mptsnun  34756  finxp1o  34809  ftc1cnnc  35129  uniqsALTV  35746  cnvepima  35754  dfom6  40239  refsum2cnlem1  41666  lptre2pt  42282  limclner  42293  limclr  42297  stoweidlem62  42704  fourierdlem42  42791  fourierdlem80  42828  fouriercnp  42868  qndenserrn  42941  salexct3  42982  salgencntex  42983  salgensscntex  42984  subsalsal  42999  0ome  43168  borelmbl  43275  mbfresmf  43373  cnfsmf  43374  incsmf  43376  smfmbfcex  43393  decsmf  43400  smfpimbor1lem2  43431  setrec2  45225