Theorem unieqd 4884

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

Syntax hints:   → wi 4   = wceq 1540  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unisn3  4892  csbuni  4900  unisn2  5267  opswap  6202  unixpid  6257  iotaeq  6476  iotabi  6477  uniabio  6478  iotanul  6489  funfv  6948  funfv2  6949  fvun  6951  dffv2  6956  fniunfv  7221  ordunisuc  7807  orduniss2  7808  onsucuni2  7809  elxp4  7898  elxp5  7899  1stval  7970  2ndval  7971  1stnpr  7972  2ndnpr  7973  fo1st  7988  fo2nd  7989  f1stres  7992  f2ndres  7993  1st2val  7996  2nd2val  7997  2nd1st  8017  cnvf1olem  8089  brtpos2  8211  dftpos4  8224  tpostpos  8225  frecseq123  8261  csbfrecsg  8263  tz7.44-2  8375  tz7.44-3  8376  rdglim2  8400  ixpsnf1o  8911  xpcomco  9031  xpassen  9035  xpdom2  9036  supeq1  9396  supeq2  9399  supeq3  9400  supeq123d  9401  supval2  9406  rankuni  9816  en2other2  9962  dfac2a  10083  dfac12lem1  10097  dfac12r  10100  kmlem9  10112  kmlem11  10114  kmlem12  10115  enfin2i  10274  fin23lem29  10294  fin23lem30  10295  fin23lem32  10297  fin23lem34  10299  fin23lem35  10300  fin23lem36  10301  fin23lem38  10302  fin23lem39  10303  fin23lem41  10305  isf34lem7  10332  isf34lem6  10333  fin1a2lem10  10362  fin1a2lem11  10363  fin1a2lem12  10364  itunisuc  10372  itunitc  10374  ttukeylem3  10464  ttukey2g  10469  pwcfsdom  10536  gruurn  10751  dfinfre  12164  relexpfld  15015  relexpfldd  15016  fsumcnv  15739  fprodcnv  15949  mrcun  17583  isacs1i  17618  mreacs  17619  arwval  18005  ipoval  18489  isacs5lem  18504  acsdrscl  18505  acsficl  18506  isps  18527  isdir  18557  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmquskerco  19216  gicqusker  19220  pmtrval  19381  pmtrfv  19382  pmtrprfv  19383  pmtrdifellem3  19408  pmtrprfval  19417  gsumcom2  19905  dmdprd  19930  dprddisj  19941  dprdf1o  19964  dprdsn  19968  dprd2da  19974  dprd2db  19975  dmdprdsplit2lem  19977  lspuni0  20916  lss0v  20923  zrhval  21417  zrhval2  21418  zrhpropd  21424  isbasisg  22834  basis1  22837  baspartn  22841  tgval  22842  eltg  22844  ntrfval  22911  ntrval  22923  tgrest  23046  restuni2  23054  lmfval  23119  cnfval  23120  cnpfval  23121  pnrmopn  23230  fiuncmp  23291  cmpfi  23295  ptval  23457  ptpjpre1  23458  elptr2  23461  ptuni2  23463  ptbasin  23464  ptbasfi  23468  xkoval  23474  txtopon  23478  ptuni  23481  ptunimpt  23482  xkouni  23486  ptpjcn  23498  ptcld  23500  dfac14  23505  ptcnp  23509  prdstopn  23515  ptrescn  23526  txcmplem2  23529  xkoptsub  23541  xkopt  23542  qtopval  23582  qtopeu  23603  hmphindis  23684  txswaphmeolem  23691  ptuncnv  23694  ptunhmeo  23695  xpstopnlem1  23696  flimval  23850  fcfval  23920  alexsubALTlem3  23936  ptcmplem1  23939  ptcmplem2  23940  ptcmplem3  23941  ptcmplem4  23942  ptcmpg  23944  cnextfres1  23955  cldsubg  23998  utopval  24120  tusval  24153  tuslem  24154  tususs  24157  ucnval  24164  prdsxmslem2  24417  ishtpy  24871  pi1buni  24940  pi1xfrcnv  24957  elovolmr  25377  ovoliunlem3  25405  uniioombllem2  25484  uniioombllem3  25486  dyadmbl  25501  vmaval  27023  vmappw  27026  madeval  27760  oldval  27762  madeoldsuc  27796  zs12bday  28343  unidifsnel  32464  unidifsnne  32465  disjabrex  32511  disjabrexf  32512  fnpreimac  32595  fcnvgreu  32597  xrge0tsmseq  33004  cycpm2tr  33076  qustrivr  33336  lmicqusker  33389  ricqusker  33398  dimval  33596  dimvalfi  33597  algextdeglem4  33710  algextdeg  33715  locfinreflem  33830  locfinref  33831  pstmval  33885  pstmfval  33886  ordtprsuni  33909  esumeq12dvaf  34021  esumeq2  34026  esumval  34036  esumf1o  34040  esumsnf  34054  esumss  34062  esumpfinval  34065  esumpfinvalf  34066  sigapildsys  34152  sxsigon  34182  meascnbl  34209  brae  34231  braew  34232  faeval  34236  imambfm  34253  cnmbfm  34254  dya2iocuni  34274  omsval  34284  omsfval  34285  omsf  34287  oms0  34288  omssubaddlem  34290  omssubadd  34291  carsgval  34294  carsgclctunlem3  34311  omsmeas  34314  elprob  34400  probfinmeasb  34419  probmeasb  34421  dstrvprob  34463  wevgblacfn  35096  indispconn  35221  iscvm  35246  cvmscld  35260  msrfval  35524  msrval  35525  mthmpps  35569  rdgprc0  35781  rdgprc  35782  dfrdg2  35783  dfrdg3  35784  unisnif  35913  brapply  35926  cbviotadavw  36257  isfne  36327  fnemeet2  36355  fnejoin2  36357  tailfval  36360  ordcmp  36435  bj-imafv  37239  mptsnunlem  37326  dissneqlem  37328  ctbssinf  37394  ptrest  37613  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  nfunidALT2  38962  nfunidALT  38963  mapdunirnN  41644  zndvdchrrhm  41960  aks6d1c7lem2  42169  aks5lem4a  42178  prjcrvfval  42619  aomclem8  43050  dfac21  43055  rp-unirabeq  43211  rp-tfslim  43342  oaun2  43370  oaun3  43371  ismnu  44250  mnuprdlem1  44261  mnuprdlem2  44262  grumnudlem  44274  grumnud  44275  ismnushort  44290  restuni6  45116  stoweidlem39  46037  salgenuni  46335  caragenval  46491  isome  46492  omeiunle  46515  isomennd  46529  unidmovn  46611  rrnmbl  46612  unidmvon  46615  hspmbl  46627  ovolval4lem2  46648  ovolval5lem2  46651  ovolval5lem3  46652  ovolval5  46653  ovnovollem2  46655  afv2eq12d  47216  uniimaelsetpreimafv  47397  fundcmpsurinjlem3  47401  imasetpreimafvbijlemfo  47406  fundcmpsurbijinjpreimafv  47408  dftpos5  48862  tposideq  48876  restcls2lem  48901  mreclat  48985  toplatglb  48989  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263  setrecseq  49674