Theorem unieqd 4877

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865

This theorem is referenced by:  unisn3  4885  csbuni  4894  unisn2  5258  opswap  6188  unixpid  6243  iotaeq  6461  iotabi  6462  uniabio  6463  iotanul  6473  funfv  6922  funfv2  6923  fvun  6925  dffv2  6930  fniunfv  7195  ordunisuc  7776  orduniss2  7777  onsucuni2  7778  elxp4  7866  elxp5  7867  1stval  7937  2ndval  7938  1stnpr  7939  2ndnpr  7940  fo1st  7955  fo2nd  7956  f1stres  7959  f2ndres  7960  1st2val  7963  2nd2val  7964  2nd1st  7984  cnvf1olem  8054  brtpos2  8176  dftpos4  8189  tpostpos  8190  frecseq123  8226  csbfrecsg  8228  tz7.44-2  8340  tz7.44-3  8341  rdglim2  8365  ixpsnf1o  8880  xpcomco  8999  xpassen  9003  xpdom2  9004  supeq1  9352  supeq2  9355  supeq3  9356  supeq123d  9357  supval2  9362  rankuni  9779  en2other2  9923  dfac2a  10044  dfac12lem1  10058  dfac12r  10061  kmlem9  10073  kmlem11  10075  kmlem12  10076  enfin2i  10235  fin23lem29  10255  fin23lem30  10256  fin23lem32  10258  fin23lem34  10260  fin23lem35  10261  fin23lem36  10262  fin23lem38  10263  fin23lem39  10264  fin23lem41  10266  isf34lem7  10293  isf34lem6  10294  fin1a2lem10  10323  fin1a2lem11  10324  fin1a2lem12  10325  itunisuc  10333  itunitc  10335  ttukeylem3  10425  ttukey2g  10430  pwcfsdom  10498  gruurn  10713  dfinfre  12127  relexpfld  14976  relexpfldd  14977  fsumcnv  15700  fprodcnv  15910  mrcun  17549  isacs1i  17584  mreacs  17585  arwval  17971  ipoval  18457  isacs5lem  18472  acsdrscl  18473  acsficl  18474  isps  18495  isdir  18525  ghmqusnsglem1  19213  ghmquskerlem1  19216  ghmquskerco  19217  gicqusker  19221  pmtrval  19384  pmtrfv  19385  pmtrprfv  19386  pmtrdifellem3  19411  pmtrprfval  19420  gsumcom2  19908  dmdprd  19933  dprddisj  19944  dprdf1o  19967  dprdsn  19971  dprd2da  19977  dprd2db  19978  dmdprdsplit2lem  19980  lspuni0  20965  lss0v  20972  zrhval  21466  zrhval2  21467  zrhpropd  21473  isbasisg  22895  basis1  22898  baspartn  22902  tgval  22903  eltg  22905  ntrfval  22972  ntrval  22984  tgrest  23107  restuni2  23115  lmfval  23180  cnfval  23181  cnpfval  23182  pnrmopn  23291  fiuncmp  23352  cmpfi  23356  ptval  23518  ptpjpre1  23519  elptr2  23522  ptuni2  23524  ptbasin  23525  ptbasfi  23529  xkoval  23535  txtopon  23539  ptuni  23542  ptunimpt  23543  xkouni  23547  ptpjcn  23559  ptcld  23561  dfac14  23566  ptcnp  23570  prdstopn  23576  ptrescn  23587  txcmplem2  23590  xkoptsub  23602  xkopt  23603  qtopval  23643  qtopeu  23664  hmphindis  23745  txswaphmeolem  23752  ptuncnv  23755  ptunhmeo  23756  xpstopnlem1  23757  flimval  23911  fcfval  23981  alexsubALTlem3  23997  ptcmplem1  24000  ptcmplem2  24001  ptcmplem3  24002  ptcmplem4  24003  ptcmpg  24005  cnextfres1  24016  cldsubg  24059  utopval  24180  tusval  24213  tuslem  24214  tususs  24217  ucnval  24224  prdsxmslem2  24477  ishtpy  24931  pi1buni  25000  pi1xfrcnv  25017  elovolmr  25437  ovoliunlem3  25465  uniioombllem2  25544  uniioombllem3  25546  dyadmbl  25561  vmaval  27083  vmappw  27086  madeval  27832  oldval  27834  madeoldsuc  27885  unidifsnel  32613  unidifsnne  32614  disjabrex  32660  disjabrexf  32661  fnpreimac  32751  fcnvgreu  32753  xrge0tsmseq  33159  cycpm2tr  33203  qustrivr  33448  lmicqusker  33501  ricqusker  33510  dimval  33759  dimvalfi  33760  algextdeglem4  33879  algextdeg  33884  locfinreflem  33999  locfinref  34000  pstmval  34054  pstmfval  34055  ordtprsuni  34078  esumeq12dvaf  34190  esumeq2  34195  esumval  34205  esumf1o  34209  esumsnf  34223  esumss  34231  esumpfinval  34234  esumpfinvalf  34235  sigapildsys  34321  sxsigon  34351  meascnbl  34378  brae  34400  braew  34401  faeval  34405  imambfm  34421  cnmbfm  34422  dya2iocuni  34442  omsval  34452  omsfval  34453  omsf  34455  oms0  34456  omssubaddlem  34458  omssubadd  34459  carsgval  34462  carsgclctunlem3  34479  omsmeas  34482  elprob  34568  probfinmeasb  34587  probmeasb  34589  dstrvprob  34631  fineqvnttrclselem1  35279  fineqvnttrclselem2  35280  fineqvnttrclselem3  35281  fineqvnttrclse  35282  fineqvr1ombregs  35296  wevgblacfn  35305  indispconn  35430  iscvm  35455  cvmscld  35469  msrfval  35733  msrval  35734  mthmpps  35778  rdgprc0  35987  rdgprc  35988  dfrdg2  35989  dfrdg3  35990  unisnif  36119  brapply  36132  cbviotadavw  36465  isfne  36535  fnemeet2  36563  fnejoin2  36565  tailfval  36568  ordcmp  36643  bj-imafv  37458  mptsnunlem  37545  dissneqlem  37547  ctbssinf  37613  ptrest  37822  mblfinlem2  37861  ovoliunnfl  37865  voliunnfl  37867  volsupnfl  37868  nfunidALT2  39297  nfunidALT  39298  mapdunirnN  41978  zndvdchrrhm  42294  aks6d1c7lem2  42503  aks5lem4a  42512  prjcrvfval  42941  aomclem8  43370  dfac21  43375  rp-unirabeq  43531  rp-tfslim  43662  oaun2  43690  oaun3  43691  ismnu  44569  mnuprdlem1  44580  mnuprdlem2  44581  grumnudlem  44593  grumnud  44594  ismnushort  44609  restuni6  45433  stoweidlem39  46350  salgenuni  46648  caragenval  46804  isome  46805  omeiunle  46828  isomennd  46842  unidmovn  46924  rrnmbl  46925  unidmvon  46928  hspmbl  46940  ovolval4lem2  46961  ovolval5lem2  46964  ovolval5lem3  46965  ovolval5  46966  ovnovollem2  46968  afv2eq12d  47528  uniimaelsetpreimafv  47709  fundcmpsurinjlem3  47713  imasetpreimafvbijlemfo  47718  fundcmpsurbijinjpreimafv  47720  dftpos5  49186  tposideq  49200  restcls2lem  49225  mreclat  49309  toplatglb  49313  swapf1a  49581  swapf2a  49583  swapf1  49584  swapf2  49586  setrecseq  49997