Theorem unieqd 4875

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863

This theorem is referenced by:  unisn3  4883  csbuni  4892  unisn2  5256  opswap  6186  unixpid  6241  iotaeq  6459  iotabi  6460  uniabio  6461  iotanul  6471  funfv  6920  funfv2  6921  fvun  6923  dffv2  6928  fniunfv  7193  ordunisuc  7774  orduniss2  7775  onsucuni2  7776  elxp4  7864  elxp5  7865  1stval  7935  2ndval  7936  1stnpr  7937  2ndnpr  7938  fo1st  7953  fo2nd  7954  f1stres  7957  f2ndres  7958  1st2val  7961  2nd2val  7962  2nd1st  7982  cnvf1olem  8052  brtpos2  8174  dftpos4  8187  tpostpos  8188  frecseq123  8224  csbfrecsg  8226  tz7.44-2  8338  tz7.44-3  8339  rdglim2  8363  ixpsnf1o  8878  xpcomco  8997  xpassen  9001  xpdom2  9002  supeq1  9350  supeq2  9353  supeq3  9354  supeq123d  9355  supval2  9360  rankuni  9777  en2other2  9921  dfac2a  10042  dfac12lem1  10056  dfac12r  10059  kmlem9  10071  kmlem11  10073  kmlem12  10074  enfin2i  10233  fin23lem29  10253  fin23lem30  10254  fin23lem32  10256  fin23lem34  10258  fin23lem35  10259  fin23lem36  10260  fin23lem38  10261  fin23lem39  10262  fin23lem41  10264  isf34lem7  10291  isf34lem6  10292  fin1a2lem10  10321  fin1a2lem11  10322  fin1a2lem12  10323  itunisuc  10331  itunitc  10333  ttukeylem3  10423  ttukey2g  10428  pwcfsdom  10496  gruurn  10711  dfinfre  12125  relexpfld  14974  relexpfldd  14975  fsumcnv  15698  fprodcnv  15908  mrcun  17547  isacs1i  17582  mreacs  17583  arwval  17969  ipoval  18455  isacs5lem  18470  acsdrscl  18471  acsficl  18472  isps  18493  isdir  18523  ghmqusnsglem1  19211  ghmquskerlem1  19214  ghmquskerco  19215  gicqusker  19219  pmtrval  19382  pmtrfv  19383  pmtrprfv  19384  pmtrdifellem3  19409  pmtrprfval  19418  gsumcom2  19906  dmdprd  19931  dprddisj  19942  dprdf1o  19965  dprdsn  19969  dprd2da  19975  dprd2db  19976  dmdprdsplit2lem  19978  lspuni0  20963  lss0v  20970  zrhval  21464  zrhval2  21465  zrhpropd  21471  isbasisg  22893  basis1  22896  baspartn  22900  tgval  22901  eltg  22903  ntrfval  22970  ntrval  22982  tgrest  23105  restuni2  23113  lmfval  23178  cnfval  23179  cnpfval  23180  pnrmopn  23289  fiuncmp  23350  cmpfi  23354  ptval  23516  ptpjpre1  23517  elptr2  23520  ptuni2  23522  ptbasin  23523  ptbasfi  23527  xkoval  23533  txtopon  23537  ptuni  23540  ptunimpt  23541  xkouni  23545  ptpjcn  23557  ptcld  23559  dfac14  23564  ptcnp  23568  prdstopn  23574  ptrescn  23585  txcmplem2  23588  xkoptsub  23600  xkopt  23601  qtopval  23641  qtopeu  23662  hmphindis  23743  txswaphmeolem  23750  ptuncnv  23753  ptunhmeo  23754  xpstopnlem1  23755  flimval  23909  fcfval  23979  alexsubALTlem3  23995  ptcmplem1  23998  ptcmplem2  23999  ptcmplem3  24000  ptcmplem4  24001  ptcmpg  24003  cnextfres1  24014  cldsubg  24057  utopval  24178  tusval  24211  tuslem  24212  tususs  24215  ucnval  24222  prdsxmslem2  24475  ishtpy  24929  pi1buni  24998  pi1xfrcnv  25015  elovolmr  25435  ovoliunlem3  25463  uniioombllem2  25542  uniioombllem3  25544  dyadmbl  25559  vmaval  27081  vmappw  27084  madeval  27828  oldval  27830  madeoldsuc  27865  unidifsnel  32590  unidifsnne  32591  disjabrex  32637  disjabrexf  32638  fnpreimac  32728  fcnvgreu  32730  xrge0tsmseq  33136  cycpm2tr  33180  qustrivr  33425  lmicqusker  33478  ricqusker  33487  dimval  33736  dimvalfi  33737  algextdeglem4  33856  algextdeg  33861  locfinreflem  33976  locfinref  33977  pstmval  34031  pstmfval  34032  ordtprsuni  34055  esumeq12dvaf  34167  esumeq2  34172  esumval  34182  esumf1o  34186  esumsnf  34200  esumss  34208  esumpfinval  34211  esumpfinvalf  34212  sigapildsys  34298  sxsigon  34328  meascnbl  34355  brae  34377  braew  34378  faeval  34382  imambfm  34398  cnmbfm  34399  dya2iocuni  34419  omsval  34429  omsfval  34430  omsf  34432  oms0  34433  omssubaddlem  34435  omssubadd  34436  carsgval  34439  carsgclctunlem3  34456  omsmeas  34459  elprob  34545  probfinmeasb  34564  probmeasb  34566  dstrvprob  34608  fineqvnttrclselem1  35256  fineqvnttrclselem2  35257  fineqvnttrclselem3  35258  fineqvnttrclse  35259  fineqvr1ombregs  35273  wevgblacfn  35282  indispconn  35407  iscvm  35432  cvmscld  35446  msrfval  35710  msrval  35711  mthmpps  35755  rdgprc0  35964  rdgprc  35965  dfrdg2  35966  dfrdg3  35967  unisnif  36096  brapply  36109  cbviotadavw  36442  isfne  36512  fnemeet2  36540  fnejoin2  36542  tailfval  36545  ordcmp  36620  bj-imafv  37425  mptsnunlem  37512  dissneqlem  37514  ctbssinf  37580  ptrest  37789  mblfinlem2  37828  ovoliunnfl  37832  voliunnfl  37834  volsupnfl  37835  nfunidALT2  39264  nfunidALT  39265  mapdunirnN  41945  zndvdchrrhm  42261  aks6d1c7lem2  42470  aks5lem4a  42479  prjcrvfval  42911  aomclem8  43340  dfac21  43345  rp-unirabeq  43501  rp-tfslim  43632  oaun2  43660  oaun3  43661  ismnu  44539  mnuprdlem1  44550  mnuprdlem2  44551  grumnudlem  44563  grumnud  44564  ismnushort  44579  restuni6  45403  stoweidlem39  46320  salgenuni  46618  caragenval  46774  isome  46775  omeiunle  46798  isomennd  46812  unidmovn  46894  rrnmbl  46895  unidmvon  46898  hspmbl  46910  ovolval4lem2  46931  ovolval5lem2  46934  ovolval5lem3  46935  ovolval5  46936  ovnovollem2  46938  afv2eq12d  47498  uniimaelsetpreimafv  47679  fundcmpsurinjlem3  47683  imasetpreimafvbijlemfo  47688  fundcmpsurbijinjpreimafv  47690  dftpos5  49156  tposideq  49170  restcls2lem  49195  mreclat  49279  toplatglb  49283  swapf1a  49551  swapf2a  49553  swapf1  49554  swapf2  49556  setrecseq  49967