Theorem unieqi 4852

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

Syntax hints:   = wceq 1539  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  elunirab  4855  unisng  4860  unidif0  5282  univ  5367  uniop  5429  dfiun3g  5873  op1sta  6128  op2nda  6131  dfdm2  6184  unixpid  6187  unisuc  6342  iotajust  6390  dfiota2  6392  cbviotaw  6398  cbviotavw  6399  cbviota  6401  sb8iota  6403  dffv4  6771  funfv2f  6857  funiunfv  7121  elunirnALT  7125  riotauni  7238  ordunisuc  7679  1st0  7837  2nd0  7838  unielxp  7869  brtpos0  8049  frrlem5  8106  frrlem8  8109  frrlem10  8111  dfwrecsOLD  8129  dfrecs3  8203  dfrecs3OLD  8204  recsfval  8212  tz7.44-3  8239  nlim1  8319  nlim2  8320  uniqs  8566  xpassen  8853  dffi3  9190  dfsup2  9203  sup00  9223  r1limg  9529  jech9.3  9572  rankxplim2  9638  rankxplim3  9639  rankxpsuc  9640  dfac5lem2  9880  kmlem11  9916  cflim2  10019  fin23lem30  10098  fin23lem34  10102  itunisuc  10175  itunitc  10177  ituniiun  10178  ac6num  10235  rankcf  10533  dprd2da  19645  dmdprdsplit2lem  19648  lssuni  20201  basdif0  22103  tgdif0  22142  neiptopuni  22281  restcls  22332  restntr  22333  pnrmopn  22494  cncmp  22543  discmp  22549  hauscmplem  22557  unisngl  22678  xkouni  22750  uptx  22776  ufildr  23082  ptcmplem3  23205  utop2nei  23402  utopreg  23404  zcld  23976  icccmp  23988  cncfcnvcn  24088  cnmpopc  24091  cnheibor  24118  evth  24122  evth2  24123  iunmbl  24717  voliun  24718  dvcnvrelem2  25182  ftc1  25206  aannenlem2  25489  circtopn  31787  locfinref  31791  zarmxt1  31830  tpr2rico  31862  cbvesum  32010  unibrsiga  32154  sxbrsigalem3  32239  dya2iocucvr  32251  sxbrsigalem1  32252  sibf0  32301  sibff  32303  sitgclg  32309  probfinmeasbALTV  32396  coinflipuniv  32448  cvmliftlem10  33256  dfon2lem7  33765  dfrdg2  33771  bday1s  34025  old0  34043  made0  34057  madeoldsuc  34067  dfiota3  34225  dffv5  34226  dfrecs2  34252  dfrdg4  34253  ordcmp  34636  bj-nuliotaALT  35229  mptsnun  35510  finxp1o  35563  ftc1cnnc  35849  uniqsALTV  36464  cnvepima  36472  sn-iotalemcor  40190  nlimsuc  41048  dfom6  41138  refsum2cnlem1  42580  lptre2pt  43181  limclner  43192  limclr  43196  stoweidlem62  43603  fourierdlem42  43690  fourierdlem80  43727  fouriercnp  43767  qndenserrn  43840  salexct3  43881  salgencntex  43882  salgensscntex  43883  subsalsal  43898  0ome  44067  borelmbl  44174  mbfresmf  44275  cnfsmf  44276  incsmf  44278  smfmbfcex  44295  decsmf  44302  smfpimbor1lem2  44333  ipoglb0  46280  setrec2  46401