Theorem unieqd 4854

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 4851	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1539  ∪ cuni 4840

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841

This theorem is referenced by:  uniprgOLD  4860  unisn3  4863  csbuni  4871  unisn2  5237  opswap  6137  unixpid  6191  iotaeq  6408  iotabi  6409  uniabio  6410  iotanul  6415  funfv  6864  funfv2  6865  fvun  6867  dffv2  6872  fniunfv  7129  ordunisuc  7688  orduniss2  7689  onsucuni2  7690  elxp4  7778  elxp5  7779  1stval  7842  2ndval  7843  1stnpr  7844  2ndnpr  7845  fo1st  7860  fo2nd  7861  f1stres  7864  f2ndres  7865  1st2val  7868  2nd2val  7869  2nd1st  7888  cnvf1olem  7959  brtpos2  8057  dftpos4  8070  tpostpos  8071  frecseq123  8107  csbfrecsg  8109  wrecseq123OLD  8140  tz7.44-2  8247  tz7.44-3  8248  rdglim2  8272  ixpsnf1o  8735  xpcomco  8858  xpassen  8862  xpdom2  8863  supeq1  9213  supeq2  9216  supeq3  9217  supeq123d  9218  supval2  9223  rankuni  9630  en2other2  9774  dfac2a  9894  dfac12lem1  9908  dfac12r  9911  kmlem9  9923  kmlem11  9925  kmlem12  9926  enfin2i  10086  fin23lem29  10106  fin23lem30  10107  fin23lem32  10109  fin23lem34  10111  fin23lem35  10112  fin23lem36  10113  fin23lem38  10114  fin23lem39  10115  fin23lem41  10117  isf34lem7  10144  isf34lem6  10145  fin1a2lem10  10174  fin1a2lem11  10175  fin1a2lem12  10176  itunisuc  10184  itunitc  10186  ttukeylem3  10276  ttukey2g  10281  pwcfsdom  10348  gruurn  10563  dfinfre  11965  relexpfld  14769  relexpfldd  14770  fsumcnv  15494  fprodcnv  15702  mrcun  17340  isacs1i  17375  mreacs  17376  arwval  17767  ipoval  18257  isacs5lem  18272  acsdrscl  18273  acsficl  18274  isps  18295  isdir  18325  pmtrval  19068  pmtrfv  19069  pmtrprfv  19070  pmtrdifellem3  19095  pmtrprfval  19104  gsumcom2  19585  dmdprd  19610  dprddisj  19621  dprdf1o  19644  dprdsn  19648  dprd2da  19654  dprd2db  19655  dmdprdsplit2lem  19657  lspuni0  20281  lss0v  20287  zrhval  20718  zrhval2  20719  zrhpropd  20725  isbasisg  22106  basis1  22109  baspartn  22113  tgval  22114  eltg  22116  ntrfval  22184  ntrval  22196  tgrest  22319  restuni2  22327  lmfval  22392  cnfval  22393  cnpfval  22394  pnrmopn  22503  fiuncmp  22564  cmpfi  22568  ptval  22730  ptpjpre1  22731  elptr2  22734  ptuni2  22736  ptbasin  22737  ptbasfi  22741  xkoval  22747  txtopon  22751  ptuni  22754  ptunimpt  22755  xkouni  22759  ptpjcn  22771  ptcld  22773  dfac14  22778  ptcnp  22782  prdstopn  22788  ptrescn  22799  txcmplem2  22802  xkoptsub  22814  xkopt  22815  qtopval  22855  qtopeu  22876  hmphindis  22957  txswaphmeolem  22964  ptuncnv  22967  ptunhmeo  22968  xpstopnlem1  22969  flimval  23123  fcfval  23193  alexsubALTlem3  23209  ptcmplem1  23212  ptcmplem2  23213  ptcmplem3  23214  ptcmplem4  23215  ptcmpg  23217  cnextfres1  23228  cldsubg  23271  utopval  23393  tusval  23426  tuslem  23427  tuslemOLD  23428  tususs  23431  ucnval  23438  prdsxmslem2  23694  ishtpy  24144  pi1buni  24212  pi1xfrcnv  24229  elovolmr  24649  ovoliunlem3  24677  uniioombllem2  24756  uniioombllem3  24758  dyadmbl  24773  vmaval  26271  vmappw  26274  unidifsnel  30892  unidifsnne  30893  disjabrex  30930  disjabrexf  30931  fnpreimac  31017  fcnvgreu  31019  xrge0tsmseq  31328  cycpm2tr  31395  qustrivr  31570  dimval  31695  dimvalfi  31696  locfinreflem  31799  locfinref  31800  pstmval  31854  pstmfval  31855  ordtprsuni  31878  esumeq12dvaf  32008  esumeq2  32013  esumval  32023  esumf1o  32027  esumsnf  32041  esumss  32049  esumpfinval  32052  esumpfinvalf  32053  sigapildsys  32139  sxsigon  32169  meascnbl  32196  brae  32218  braew  32219  faeval  32223  imambfm  32238  cnmbfm  32239  dya2iocuni  32259  omsval  32269  omsfval  32270  omsf  32272  oms0  32273  omssubaddlem  32275  omssubadd  32276  carsgval  32279  carsgclctunlem3  32296  omsmeas  32299  elprob  32385  probfinmeasb  32404  probmeasb  32406  dstrvprob  32447  indispconn  33205  iscvm  33230  cvmscld  33244  msrfval  33508  msrval  33509  mthmpps  33553  rdgprc0  33778  rdgprc  33779  dfrdg2  33780  dfrdg3  33781  madeval  34045  oldval  34047  madeoldsuc  34076  unisnif  34236  brapply  34249  isfne  34537  fnemeet2  34565  fnejoin2  34567  tailfval  34570  ordcmp  34645  bj-imafv  35431  mptsnunlem  35518  dissneqlem  35520  ctbssinf  35586  ptrest  35785  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  nfunidALT2  36990  nfunidALT  36991  mapdunirnN  39671  prjcrvfval  40475  aomclem8  40893  dfac21  40898  ismnu  41886  mnuprdlem1  41897  mnuprdlem2  41898  grumnudlem  41910  grumnud  41911  ismnushort  41926  restuni6  42678  stoweidlem39  43587  salgenuni  43883  caragenval  44038  isome  44039  omeiunle  44062  isomennd  44076  unidmovn  44158  rrnmbl  44159  unidmvon  44162  hspmbl  44174  ovolval4lem2  44195  ovolval5lem2  44198  ovolval5lem3  44199  ovolval5  44200  ovnovollem2  44202  afv2eq12d  44718  uniimaelsetpreimafv  44859  fundcmpsurinjlem3  44863  imasetpreimafvbijlemfo  44868  fundcmpsurbijinjpreimafv  44870  restcls2lem  46217  mreclat  46294  toplatglb  46298  setrecseq  46402