Theorem unieqd 4918

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

Syntax hints:   → wi 4   = wceq 1534  ∪ cuni 4905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3963  df-uni 4906

This theorem is referenced by:  uniprgOLD  4924  unisn3  4928  csbuni  4936  unisn2  5309  opswap  6232  unixpid  6287  iotaeq  6511  iotabi  6512  uniabio  6513  iotanul  6524  funfv  6981  funfv2  6982  fvun  6984  dffv2  6989  fniunfv  7254  ordunisuc  7833  orduniss2  7834  onsucuni2  7835  elxp4  7927  elxp5  7928  1stval  7997  2ndval  7998  1stnpr  7999  2ndnpr  8000  fo1st  8015  fo2nd  8016  f1stres  8019  f2ndres  8020  1st2val  8023  2nd2val  8024  2nd1st  8044  cnvf1olem  8116  brtpos2  8239  dftpos4  8252  tpostpos  8253  frecseq123  8289  csbfrecsg  8291  wrecseq123OLD  8322  tz7.44-2  8429  tz7.44-3  8430  rdglim2  8454  ixpsnf1o  8959  xpcomco  9092  xpassen  9096  xpdom2  9097  supeq1  9481  supeq2  9484  supeq3  9485  supeq123d  9486  supval2  9491  rankuni  9899  en2other2  10045  dfac2a  10165  dfac12lem1  10179  dfac12r  10182  kmlem9  10194  kmlem11  10196  kmlem12  10197  enfin2i  10355  fin23lem29  10375  fin23lem30  10376  fin23lem32  10378  fin23lem34  10380  fin23lem35  10381  fin23lem36  10382  fin23lem38  10383  fin23lem39  10384  fin23lem41  10386  isf34lem7  10413  isf34lem6  10414  fin1a2lem10  10443  fin1a2lem11  10444  fin1a2lem12  10445  itunisuc  10453  itunitc  10455  ttukeylem3  10545  ttukey2g  10550  pwcfsdom  10617  gruurn  10832  dfinfre  12241  relexpfld  15049  relexpfldd  15050  fsumcnv  15772  fprodcnv  15980  mrcun  17630  isacs1i  17665  mreacs  17666  arwval  18060  ipoval  18550  isacs5lem  18565  acsdrscl  18566  acsficl  18567  isps  18588  isdir  18618  ghmqusnsglem1  19270  ghmquskerlem1  19273  ghmquskerco  19274  gicqusker  19278  pmtrval  19445  pmtrfv  19446  pmtrprfv  19447  pmtrdifellem3  19472  pmtrprfval  19481  gsumcom2  19969  dmdprd  19994  dprddisj  20005  dprdf1o  20028  dprdsn  20032  dprd2da  20038  dprd2db  20039  dmdprdsplit2lem  20041  lspuni0  20983  lss0v  20990  zrhval  21493  zrhval2  21494  zrhpropd  21500  isbasisg  22938  basis1  22941  baspartn  22945  tgval  22946  eltg  22948  ntrfval  23016  ntrval  23028  tgrest  23151  restuni2  23159  lmfval  23224  cnfval  23225  cnpfval  23226  pnrmopn  23335  fiuncmp  23396  cmpfi  23400  ptval  23562  ptpjpre1  23563  elptr2  23566  ptuni2  23568  ptbasin  23569  ptbasfi  23573  xkoval  23579  txtopon  23583  ptuni  23586  ptunimpt  23587  xkouni  23591  ptpjcn  23603  ptcld  23605  dfac14  23610  ptcnp  23614  prdstopn  23620  ptrescn  23631  txcmplem2  23634  xkoptsub  23646  xkopt  23647  qtopval  23687  qtopeu  23708  hmphindis  23789  txswaphmeolem  23796  ptuncnv  23799  ptunhmeo  23800  xpstopnlem1  23801  flimval  23955  fcfval  24025  alexsubALTlem3  24041  ptcmplem1  24044  ptcmplem2  24045  ptcmplem3  24046  ptcmplem4  24047  ptcmpg  24049  cnextfres1  24060  cldsubg  24103  utopval  24225  tusval  24258  tuslem  24259  tuslemOLD  24260  tususs  24263  ucnval  24270  prdsxmslem2  24526  ishtpy  24986  pi1buni  25055  pi1xfrcnv  25072  elovolmr  25493  ovoliunlem3  25521  uniioombllem2  25600  uniioombllem3  25602  dyadmbl  25617  vmaval  27138  vmappw  27141  madeval  27873  oldval  27875  madeoldsuc  27905  unidifsnel  32461  unidifsnne  32462  disjabrex  32502  disjabrexf  32503  fnpreimac  32588  fcnvgreu  32590  xrge0tsmseq  32932  cycpm2tr  33001  qustrivr  33246  lmicqusker  33299  ricqusker  33308  dimval  33501  dimvalfi  33502  algextdeglem4  33593  algextdeg  33598  locfinreflem  33668  locfinref  33669  pstmval  33723  pstmfval  33724  ordtprsuni  33747  esumeq12dvaf  33877  esumeq2  33882  esumval  33892  esumf1o  33896  esumsnf  33910  esumss  33918  esumpfinval  33921  esumpfinvalf  33922  sigapildsys  34008  sxsigon  34038  meascnbl  34065  brae  34087  braew  34088  faeval  34092  imambfm  34109  cnmbfm  34110  dya2iocuni  34130  omsval  34140  omsfval  34141  omsf  34143  oms0  34144  omssubaddlem  34146  omssubadd  34147  carsgval  34150  carsgclctunlem3  34167  omsmeas  34170  elprob  34256  probfinmeasb  34275  probmeasb  34277  dstrvprob  34318  wevgblacfn  34949  indispconn  35075  iscvm  35100  cvmscld  35114  msrfval  35378  msrval  35379  mthmpps  35423  rdgprc0  35630  rdgprc  35631  dfrdg2  35632  dfrdg3  35633  unisnif  35762  brapply  35775  isfne  36064  fnemeet2  36092  fnejoin2  36094  tailfval  36097  ordcmp  36172  bj-imafv  36971  mptsnunlem  37058  dissneqlem  37060  ctbssinf  37126  ptrest  37333  mblfinlem2  37372  ovoliunnfl  37376  voliunnfl  37378  volsupnfl  37379  nfunidALT2  38680  nfunidALT  38681  mapdunirnN  41362  zndvdchrrhm  41682  aks6d1c7lem2  41893  aks5lem4a  41902  prjcrvfval  42321  aomclem8  42759  dfac21  42764  rp-unirabeq  42924  rp-tfslim  43056  oaun2  43084  oaun3  43085  ismnu  43972  mnuprdlem1  43983  mnuprdlem2  43984  grumnudlem  43996  grumnud  43997  ismnushort  44012  restuni6  44760  stoweidlem39  45696  salgenuni  45994  caragenval  46150  isome  46151  omeiunle  46174  isomennd  46188  unidmovn  46270  rrnmbl  46271  unidmvon  46274  hspmbl  46286  ovolval4lem2  46307  ovolval5lem2  46310  ovolval5lem3  46311  ovolval5  46312  ovnovollem2  46314  afv2eq12d  46864  uniimaelsetpreimafv  47004  fundcmpsurinjlem3  47008  imasetpreimafvbijlemfo  47013  fundcmpsurbijinjpreimafv  47015  restcls2lem  48282  mreclat  48359  toplatglb  48363  setrecseq  48467