Theorem unieqd 4863

Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)

Hypothesis

Ref	Expression
unieqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
unieqd	⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Proof of Theorem unieqd

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		unieq 4861	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ∪ cuni 4850

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  unisn3  4871  csbuni  4880  unisn2  5247  opswap  6193  unixpid  6248  iotaeq  6466  iotabi  6467  uniabio  6468  iotanul  6478  funfv  6927  funfv2  6928  fvun  6930  dffv2  6935  fniunfv  7202  ordunisuc  7783  orduniss2  7784  onsucuni2  7785  elxp4  7873  elxp5  7874  1stval  7944  2ndval  7945  1stnpr  7946  2ndnpr  7947  fo1st  7962  fo2nd  7963  f1stres  7966  f2ndres  7967  1st2val  7970  2nd2val  7971  2nd1st  7991  cnvf1olem  8060  brtpos2  8182  dftpos4  8195  tpostpos  8196  frecseq123  8232  csbfrecsg  8234  tz7.44-2  8346  tz7.44-3  8347  rdglim2  8371  ixpsnf1o  8886  xpcomco  9005  xpassen  9009  xpdom2  9010  supeq1  9358  supeq2  9361  supeq3  9362  supeq123d  9363  supval2  9368  rankuni  9787  en2other2  9931  dfac2a  10052  dfac12lem1  10066  dfac12r  10069  kmlem9  10081  kmlem11  10083  kmlem12  10084  enfin2i  10243  fin23lem29  10263  fin23lem30  10264  fin23lem32  10266  fin23lem34  10268  fin23lem35  10269  fin23lem36  10270  fin23lem38  10271  fin23lem39  10272  fin23lem41  10274  isf34lem7  10301  isf34lem6  10302  fin1a2lem10  10331  fin1a2lem11  10332  fin1a2lem12  10333  itunisuc  10341  itunitc  10343  ttukeylem3  10433  ttukey2g  10438  pwcfsdom  10506  gruurn  10721  dfinfre  12137  relexpfld  15011  relexpfldd  15012  fsumcnv  15735  fprodcnv  15948  mrcun  17588  isacs1i  17623  mreacs  17624  arwval  18010  ipoval  18496  isacs5lem  18511  acsdrscl  18512  acsficl  18513  isps  18534  isdir  18564  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmquskerco  19259  gicqusker  19263  pmtrval  19426  pmtrfv  19427  pmtrprfv  19428  pmtrdifellem3  19453  pmtrprfval  19462  gsumcom2  19950  dmdprd  19975  dprddisj  19986  dprdf1o  20009  dprdsn  20013  dprd2da  20019  dprd2db  20020  dmdprdsplit2lem  20022  lspuni0  21005  lss0v  21011  zrhval  21487  zrhval2  21488  zrhpropd  21494  isbasisg  22912  basis1  22915  baspartn  22919  tgval  22920  eltg  22922  ntrfval  22989  ntrval  23001  tgrest  23124  restuni2  23132  lmfval  23197  cnfval  23198  cnpfval  23199  pnrmopn  23308  fiuncmp  23369  cmpfi  23373  ptval  23535  ptpjpre1  23536  elptr2  23539  ptuni2  23541  ptbasin  23542  ptbasfi  23546  xkoval  23552  txtopon  23556  ptuni  23559  ptunimpt  23560  xkouni  23564  ptpjcn  23576  ptcld  23578  dfac14  23583  ptcnp  23587  prdstopn  23593  ptrescn  23604  txcmplem2  23607  xkoptsub  23619  xkopt  23620  qtopval  23660  qtopeu  23681  hmphindis  23762  txswaphmeolem  23769  ptuncnv  23772  ptunhmeo  23773  xpstopnlem1  23774  flimval  23928  fcfval  23998  alexsubALTlem3  24014  ptcmplem1  24017  ptcmplem2  24018  ptcmplem3  24019  ptcmplem4  24020  ptcmpg  24022  cnextfres1  24033  cldsubg  24076  utopval  24197  tusval  24230  tuslem  24231  tususs  24234  ucnval  24241  prdsxmslem2  24494  ishtpy  24939  pi1buni  25007  pi1xfrcnv  25024  elovolmr  25443  ovoliunlem3  25471  uniioombllem2  25550  uniioombllem3  25552  dyadmbl  25567  vmaval  27076  vmappw  27079  madeval  27824  oldval  27826  madeoldsuc  27877  unidifsnel  32605  unidifsnne  32606  disjabrex  32652  disjabrexf  32653  fnpreimac  32743  fcnvgreu  32745  xrge0tsmseq  33136  cycpm2tr  33180  qustrivr  33425  lmicqusker  33478  ricqusker  33487  esplyfval1  33717  dimval  33745  dimvalfi  33746  algextdeglem4  33864  algextdeg  33869  locfinreflem  33984  locfinref  33985  pstmval  34039  pstmfval  34040  ordtprsuni  34063  esumeq12dvaf  34175  esumeq2  34180  esumval  34190  esumf1o  34194  esumsnf  34208  esumss  34216  esumpfinval  34219  esumpfinvalf  34220  sigapildsys  34306  sxsigon  34336  meascnbl  34363  brae  34385  braew  34386  faeval  34390  imambfm  34406  cnmbfm  34407  dya2iocuni  34427  omsval  34437  omsfval  34438  omsf  34440  oms0  34441  omssubaddlem  34443  omssubadd  34444  carsgval  34447  carsgclctunlem3  34464  omsmeas  34467  elprob  34553  probfinmeasb  34572  probmeasb  34574  dstrvprob  34616  fineqvnttrclselem1  35265  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  fineqvnttrclse  35268  fineqvr1ombregs  35282  wevgblacfn  35291  indispconn  35416  iscvm  35441  cvmscld  35455  msrfval  35719  msrval  35720  mthmpps  35764  rdgprc0  35973  rdgprc  35974  dfrdg2  35975  dfrdg3  35976  unisnif  36105  brapply  36118  cbviotadavw  36451  isfne  36521  fnemeet2  36549  fnejoin2  36551  tailfval  36554  ordcmp  36629  ttcid  36674  bj-imafv  37565  mptsnunlem  37654  dissneqlem  37656  ctbssinf  37722  ptrest  37940  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  nfunidALT2  39415  nfunidALT  39416  mapdunirnN  42096  zndvdchrrhm  42412  aks6d1c7lem2  42620  aks5lem4a  42629  prjcrvfval  43064  aomclem8  43489  dfac21  43494  rp-unirabeq  43650  rp-tfslim  43781  oaun2  43809  oaun3  43810  ismnu  44688  mnuprdlem1  44699  mnuprdlem2  44700  grumnudlem  44712  grumnud  44713  ismnushort  44728  restuni6  45552  stoweidlem39  46467  salgenuni  46765  caragenval  46921  isome  46922  omeiunle  46945  isomennd  46959  unidmovn  47041  rrnmbl  47042  unidmvon  47045  hspmbl  47057  ovolval4lem2  47078  ovolval5lem2  47081  ovolval5lem3  47082  ovolval5  47083  ovnovollem2  47085  afv2eq12d  47663  uniimaelsetpreimafv  47856  fundcmpsurinjlem3  47860  imasetpreimafvbijlemfo  47865  fundcmpsurbijinjpreimafv  47867  dftpos5  49349  tposideq  49363  restcls2lem  49388  mreclat  49472  toplatglb  49476  swapf1a  49744  swapf2a  49746  swapf1  49747  swapf2  49749  setrecseq  50160