Theorem unieqd 4871

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

Syntax hints:   → wi 4   = wceq 1541  ∪ cuni 4857

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-in 3909  df-ss 3919  df-uni 4858

This theorem is referenced by:  uniprgOLD  4877  unisn3  4881  csbuni  4889  unisn2  5261  opswap  6172  unixpid  6227  iotaeq  6449  iotabi  6450  uniabio  6451  iotanul  6462  funfv  6916  funfv2  6917  fvun  6919  dffv2  6924  fniunfv  7181  ordunisuc  7750  orduniss2  7751  onsucuni2  7752  elxp4  7842  elxp5  7843  1stval  7906  2ndval  7907  1stnpr  7908  2ndnpr  7909  fo1st  7924  fo2nd  7925  f1stres  7928  f2ndres  7929  1st2val  7932  2nd2val  7933  2nd1st  7952  cnvf1olem  8023  brtpos2  8123  dftpos4  8136  tpostpos  8137  frecseq123  8173  csbfrecsg  8175  wrecseq123OLD  8206  tz7.44-2  8313  tz7.44-3  8314  rdglim2  8338  ixpsnf1o  8802  xpcomco  8932  xpassen  8936  xpdom2  8937  supeq1  9307  supeq2  9310  supeq3  9311  supeq123d  9312  supval2  9317  rankuni  9725  en2other2  9871  dfac2a  9991  dfac12lem1  10005  dfac12r  10008  kmlem9  10020  kmlem11  10022  kmlem12  10023  enfin2i  10183  fin23lem29  10203  fin23lem30  10204  fin23lem32  10206  fin23lem34  10208  fin23lem35  10209  fin23lem36  10210  fin23lem38  10211  fin23lem39  10212  fin23lem41  10214  isf34lem7  10241  isf34lem6  10242  fin1a2lem10  10271  fin1a2lem11  10272  fin1a2lem12  10273  itunisuc  10281  itunitc  10283  ttukeylem3  10373  ttukey2g  10378  pwcfsdom  10445  gruurn  10660  dfinfre  12062  relexpfld  14860  relexpfldd  14861  fsumcnv  15585  fprodcnv  15793  mrcun  17429  isacs1i  17464  mreacs  17465  arwval  17856  ipoval  18346  isacs5lem  18361  acsdrscl  18362  acsficl  18363  isps  18384  isdir  18414  pmtrval  19156  pmtrfv  19157  pmtrprfv  19158  pmtrdifellem3  19183  pmtrprfval  19192  gsumcom2  19671  dmdprd  19696  dprddisj  19707  dprdf1o  19730  dprdsn  19734  dprd2da  19740  dprd2db  19741  dmdprdsplit2lem  19743  lspuni0  20378  lss0v  20384  zrhval  20815  zrhval2  20816  zrhpropd  20822  isbasisg  22203  basis1  22206  baspartn  22210  tgval  22211  eltg  22213  ntrfval  22281  ntrval  22293  tgrest  22416  restuni2  22424  lmfval  22489  cnfval  22490  cnpfval  22491  pnrmopn  22600  fiuncmp  22661  cmpfi  22665  ptval  22827  ptpjpre1  22828  elptr2  22831  ptuni2  22833  ptbasin  22834  ptbasfi  22838  xkoval  22844  txtopon  22848  ptuni  22851  ptunimpt  22852  xkouni  22856  ptpjcn  22868  ptcld  22870  dfac14  22875  ptcnp  22879  prdstopn  22885  ptrescn  22896  txcmplem2  22899  xkoptsub  22911  xkopt  22912  qtopval  22952  qtopeu  22973  hmphindis  23054  txswaphmeolem  23061  ptuncnv  23064  ptunhmeo  23065  xpstopnlem1  23066  flimval  23220  fcfval  23290  alexsubALTlem3  23306  ptcmplem1  23309  ptcmplem2  23310  ptcmplem3  23311  ptcmplem4  23312  ptcmpg  23314  cnextfres1  23325  cldsubg  23368  utopval  23490  tusval  23523  tuslem  23524  tuslemOLD  23525  tususs  23528  ucnval  23535  prdsxmslem2  23791  ishtpy  24241  pi1buni  24309  pi1xfrcnv  24326  elovolmr  24746  ovoliunlem3  24774  uniioombllem2  24853  uniioombllem3  24855  dyadmbl  24870  vmaval  26368  vmappw  26371  unidifsnel  31168  unidifsnne  31169  disjabrex  31206  disjabrexf  31207  fnpreimac  31293  fcnvgreu  31295  xrge0tsmseq  31604  cycpm2tr  31671  qustrivr  31855  dimval  31982  dimvalfi  31983  locfinreflem  32086  locfinref  32087  pstmval  32141  pstmfval  32142  ordtprsuni  32165  esumeq12dvaf  32295  esumeq2  32300  esumval  32310  esumf1o  32314  esumsnf  32328  esumss  32336  esumpfinval  32339  esumpfinvalf  32340  sigapildsys  32426  sxsigon  32456  meascnbl  32483  brae  32505  braew  32506  faeval  32510  imambfm  32527  cnmbfm  32528  dya2iocuni  32548  omsval  32558  omsfval  32559  omsf  32561  oms0  32562  omssubaddlem  32564  omssubadd  32565  carsgval  32568  carsgclctunlem3  32585  omsmeas  32588  elprob  32674  probfinmeasb  32693  probmeasb  32695  dstrvprob  32736  indispconn  33493  iscvm  33518  cvmscld  33532  msrfval  33796  msrval  33797  mthmpps  33841  rdgprc0  34052  rdgprc  34053  dfrdg2  34054  dfrdg3  34055  madeval  34144  oldval  34146  madeoldsuc  34175  unisnif  34364  brapply  34377  isfne  34665  fnemeet2  34693  fnejoin2  34695  tailfval  34698  ordcmp  34773  bj-imafv  35576  mptsnunlem  35663  dissneqlem  35665  ctbssinf  35731  ptrest  35930  mblfinlem2  35969  ovoliunnfl  35973  voliunnfl  35975  volsupnfl  35976  nfunidALT2  37285  nfunidALT  37286  mapdunirnN  39967  prjcrvfval  40779  aomclem8  41198  dfac21  41203  ismnu  42250  mnuprdlem1  42261  mnuprdlem2  42262  grumnudlem  42274  grumnud  42275  ismnushort  42290  restuni6  43042  stoweidlem39  43966  salgenuni  44262  caragenval  44418  isome  44419  omeiunle  44442  isomennd  44456  unidmovn  44538  rrnmbl  44539  unidmvon  44542  hspmbl  44554  ovolval4lem2  44575  ovolval5lem2  44578  ovolval5lem3  44579  ovolval5  44580  ovnovollem2  44582  afv2eq12d  45123  uniimaelsetpreimafv  45264  fundcmpsurinjlem3  45268  imasetpreimafvbijlemfo  45273  fundcmpsurbijinjpreimafv  45275  restcls2lem  46622  mreclat  46699  toplatglb  46703  setrecseq  46807