Theorem unieqi 4886

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

Syntax hints:   = wceq 1567  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-uni 4875

This theorem is referenced by:  elunirab  4889  unisng  4892  unidif0  5331  unidif0OLD  5332  univ  5433  uniop  5499  dfiun3g  5959  op1sta  6227  op2nda  6230  dfdm2  6283  unixpid  6286  unisucs  6441  iotajust  6492  dfiota2  6494  cbviotaw  6500  cbviotavw  6501  cbviota  6502  sb8iota  6504  dffv4  6879  funfv2f  6971  funiunfv  7247  elunirnALT  7251  riotauni  7374  ordunisuc  7828  1st0  7992  2nd0  7993  unielxp  8024  brtpos0  8229  frrlem5  8287  frrlem8  8290  frrlem10  8292  dfrecs3  8359  recsfval  8367  tz7.44-3  8395  nlim1  8474  nlim2  8475  uniqs  8771  xpassen  9059  dffi3  9391  dfsup2  9404  sup00  9425  r1limg  9743  jech9.3  9786  rankxplim2  9852  rankxplim3  9853  rankxpsuc  9854  dfac5lem2  10108  kmlem11  10144  cflim2  10247  fin23lem30  10326  fin23lem34  10330  itunisuc  10403  itunitc  10405  ituniiun  10406  ac6num  10463  rankcf  10762  dprd2da  20114  dmdprdsplit2lem  20117  lssuni  21038  basdif0  23079  tgdif0  23118  neiptopuni  23256  restcls  23307  restntr  23308  pnrmopn  23469  cncmp  23518  discmp  23524  hauscmplem  23532  unisngl  23653  xkouni  23725  uptx  23751  ufildr  24057  ptcmplem3  24180  utop2nei  24376  utopreg  24378  zcld  24940  icccmp  24952  cncfcnvcn  25053  cnmpopc  25056  cnheibor  25083  evth  25087  evth2  25088  iunmbl  25681  voliun  25682  dvcnvrelem2  26146  ftc1  26170  aannenlem2  26459  bday1  27973  old0  27998  made0  28022  old1  28024  madeoldsuc  28044  isconstr  34071  circtopn  34172  locfinref  34176  zarmxt1  34215  tpr2rico  34247  cbvesum  34377  cbvesumv  34378  unibrsiga  34521  sxbrsigalem3  34607  dya2iocucvr  34619  sxbrsigalem1  34620  sibf0  34669  sibff  34671  sitgclg  34677  probfinmeasbALTV  34764  coinflipuniv  34817  fineqvnttrclse  35470  wevgblacfn  35528  cvmliftlem10  35719  dfon2lem7  36212  dfrdg2  36218  dfiota3  36346  dffv5  36347  dfrecs2  36375  dfrdg4  36376  ordcmp  36881  ttcuni  36947  bj-nuliotaALT  37617  mptsnun  37908  finxp1o  37961  ftc1cnnc  38266  cnvepima  38911  sn-iotalemcor  42918  onsucunitp  44027  dfom6  44184  refsum2cnlem1  45684  lptre2pt  46281  limclner  46292  limclr  46296  stoweidlem62  46703  fourierdlem42  46790  fourierdlem80  46827  fouriercnp  46867  qndenserrn  46940  salexct3  46983  salgencntex  46984  salgensscntex  46985  subsalsal  47000  0ome  47170  borelmbl  47277  mbfresmf  47380  cnfsmf  47381  incsmf  47383  smfmbfcex  47401  decsmf  47408  smfpimbor1lem2  47440  dftpos5  49572  ipoglb0  49692  setrec2  50393