Theorem unieqd 4446

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

Syntax hints:   → wi 4   = wceq 1483  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437

This theorem is referenced by:  uniprg  4450  unisng  4452  unisn3  4453  csbuni  4466  unisn2  4794  opswap  5622  unixpid  5670  iotaeq  5859  iotabi  5860  uniabio  5861  iotanul  5866  funfv  6265  funfv2  6266  fvun  6268  dffv2  6271  fniunfv  6505  ordunisuc  7032  orduniss2  7033  onsucuni2  7034  elxp4  7110  elxp5  7111  1stval  7170  2ndval  7171  1stnpr  7172  2ndnpr  7173  fo1st  7188  fo2nd  7189  f1stres  7190  f2ndres  7191  1st2val  7194  2nd2val  7195  2nd1st  7213  cnvf1olem  7275  brtpos2  7358  dftpos4  7371  tpostpos  7372  wrecseq123  7408  tz7.44-2  7503  tz7.44-3  7504  rdglim2  7528  ixpsnf1o  7948  xpcomco  8050  xpassen  8054  xpdom2  8055  supeq1  8351  supeq2  8354  supeq3  8355  supeq123d  8356  supval2  8361  rankuni  8726  en2other2  8832  dfac2a  8952  dfac12lem1  8965  dfac12r  8968  kmlem9  8980  kmlem11  8982  kmlem12  8983  enfin2i  9143  fin23lem29  9163  fin23lem30  9164  fin23lem32  9166  fin23lem34  9168  fin23lem35  9169  fin23lem36  9170  fin23lem38  9171  fin23lem39  9172  fin23lem41  9174  isf34lem7  9201  isf34lem6  9202  fin1a2lem10  9231  fin1a2lem11  9232  fin1a2lem12  9233  itunisuc  9241  itunitc  9243  ttukeylem3  9333  ttukey2g  9338  pwcfsdom  9405  gruurn  9620  dfinfre  11004  relexpfld  13789  fsumcnv  14504  fprodcnv  14713  mrcun  16282  isacs1i  16318  mreacs  16319  arwval  16693  ipoval  17154  isacs5lem  17169  acsdrscl  17170  acsficl  17171  isps  17202  isdir  17232  pmtrval  17871  pmtrfv  17872  pmtrprfv  17873  pmtrdifellem3  17898  pmtrprfval  17907  gsumcom2  18374  dmdprd  18397  dprddisj  18408  dprdf1o  18431  dprdsn  18435  dprd2da  18441  dprd2db  18442  dmdprdsplit2lem  18444  lspuni0  19010  lss0v  19016  zrhval  19856  zrhval2  19857  zrhpropd  19863  isbasisg  20751  basis1  20754  baspartn  20758  tgval  20759  eltg  20761  ntrfval  20828  ntrval  20840  tgrest  20963  restuni2  20971  lmfval  21036  cnfval  21037  cnpfval  21038  pnrmopn  21147  fiuncmp  21207  cmpfi  21211  ptval  21373  ptpjpre1  21374  elptr2  21377  ptuni2  21379  ptbasin  21380  ptbasfi  21384  xkoval  21390  txtopon  21394  ptuni  21397  ptunimpt  21398  xkouni  21402  ptpjcn  21414  ptcld  21416  dfac14  21421  ptcnp  21425  prdstopn  21431  ptrescn  21442  txcmplem2  21445  xkoptsub  21457  xkopt  21458  qtopval  21498  qtopeu  21519  hmphindis  21600  txswaphmeolem  21607  ptuncnv  21610  ptunhmeo  21611  xpstopnlem1  21612  flimval  21767  fcfval  21837  alexsubALTlem3  21853  ptcmplem1  21856  ptcmplem2  21857  ptcmplem3  21858  ptcmplem4  21859  ptcmpg  21861  cnextfres1  21872  cldsubg  21914  utopval  22036  tusval  22070  tuslem  22071  tususs  22074  ucnval  22081  prdsxmslem2  22334  ishtpy  22771  pi1buni  22840  pi1xfrcnv  22857  elovolmr  23244  ovoliunlem3  23272  uniioombllem2  23351  uniioombllem3  23353  dyadmbl  23368  vmaval  24839  vmappw  24842  disjabrex  29395  disjabrexf  29396  fcnvgreu  29472  xrge0tsmseq  29787  locfinreflem  29907  locfinref  29908  pstmval  29938  pstmfval  29939  ordtprsuni  29965  esumeq12dvaf  30093  esumeq2  30098  esumval  30108  esumf1o  30112  esumsnf  30126  esumss  30134  esumpfinval  30137  esumpfinvalf  30138  sigapildsys  30225  sxsigon  30255  meascnbl  30282  brae  30304  braew  30305  faeval  30309  imambfm  30324  cnmbfm  30325  dya2iocuni  30345  omsval  30355  omsfval  30356  omsf  30358  oms0  30359  omssubaddlem  30361  omssubadd  30362  carsgval  30365  carsgclctunlem3  30382  omsmeas  30385  elprob  30471  probfinmeasb  30491  probmeasb  30492  dstrvprob  30533  indispconn  31216  iscvm  31241  cvmscld  31255  msrfval  31434  msrval  31435  mthmpps  31479  rdgprc0  31699  rdgprc  31700  dfrdg2  31701  dfrdg3  31702  trpredeq1  31720  trpredeq2  31721  trpredeq3  31722  madeval  31935  unisnif  32032  brapply  32045  isfne  32334  fnemeet2  32362  fnejoin2  32364  tailfval  32367  ordcmp  32446  csbwrecsg  33173  mptsnunlem  33185  dissneqlem  33187  ptrest  33408  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  nfunidALT2  34256  nfunidALT  34257  mapdunirnN  36939  aomclem8  37631  dfac21  37636  csbfv12gALTOLD  39052  restuni6  39305  stoweidlem39  40256  salgenuni  40555  caragenval  40707  isome  40708  omeiunle  40731  isomennd  40745  unidmovn  40827  rrnmbl  40828  unidmvon  40831  hspmbl  40843  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovollem2  40871  setrecseq  42432