Theorem unieqd 4651

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

Syntax hints:   → wi 4   = wceq 1637  ∪ cuni 4641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-uni 4642

This theorem is referenced by:  uniprg  4655  unisngOLD  4659  unisn3  4660  csbuni  4671  unisn2  5002  opswap  5850  unixpid  5898  iotaeq  6082  iotabi  6083  uniabio  6084  iotanul  6089  funfv  6496  funfv2  6497  fvun  6499  dffv2  6502  fniunfv  6739  ordunisuc  7272  orduniss2  7273  onsucuni2  7274  elxp4  7350  elxp5  7351  1stval  7410  2ndval  7411  1stnpr  7412  2ndnpr  7413  fo1st  7428  fo2nd  7429  f1stres  7432  f2ndres  7433  1st2val  7436  2nd2val  7437  2nd1st  7455  cnvf1olem  7519  brtpos2  7603  dftpos4  7616  tpostpos  7617  wrecseq123  7653  tz7.44-2  7749  tz7.44-3  7750  rdglim2  7774  ixpsnf1o  8195  xpcomco  8299  xpassen  8303  xpdom2  8304  supeq1  8600  supeq2  8603  supeq3  8604  supeq123d  8605  supval2  8610  rankuni  8983  en2other2  9125  dfac2a  9245  dfac12lem1  9260  dfac12r  9263  kmlem9  9275  kmlem11  9277  kmlem12  9278  enfin2i  9438  fin23lem29  9458  fin23lem30  9459  fin23lem32  9461  fin23lem34  9463  fin23lem35  9464  fin23lem36  9465  fin23lem38  9466  fin23lem39  9467  fin23lem41  9469  isf34lem7  9496  isf34lem6  9497  fin1a2lem10  9526  fin1a2lem11  9527  fin1a2lem12  9528  itunisuc  9536  itunitc  9538  ttukeylem3  9628  ttukey2g  9633  pwcfsdom  9700  gruurn  9915  dfinfre  11299  relexpfld  14032  fsumcnv  14747  fprodcnv  14954  mrcun  16507  isacs1i  16542  mreacs  16543  arwval  16917  ipoval  17379  isacs5lem  17394  acsdrscl  17395  acsficl  17396  isps  17427  isdir  17457  pmtrval  18092  pmtrfv  18093  pmtrprfv  18094  pmtrdifellem3  18119  pmtrprfval  18128  gsumcom2  18595  dmdprd  18619  dprddisj  18630  dprdf1o  18653  dprdsn  18657  dprd2da  18663  dprd2db  18664  dmdprdsplit2lem  18666  lspuni0  19237  lss0v  19243  zrhval  20084  zrhval2  20085  zrhpropd  20091  isbasisg  20986  basis1  20989  baspartn  20993  tgval  20994  eltg  20996  ntrfval  21063  ntrval  21075  tgrest  21198  restuni2  21206  lmfval  21271  cnfval  21272  cnpfval  21273  pnrmopn  21382  fiuncmp  21442  cmpfi  21446  ptval  21608  ptpjpre1  21609  elptr2  21612  ptuni2  21614  ptbasin  21615  ptbasfi  21619  xkoval  21625  txtopon  21629  ptuni  21632  ptunimpt  21633  xkouni  21637  ptpjcn  21649  ptcld  21651  dfac14  21656  ptcnp  21660  prdstopn  21666  ptrescn  21677  txcmplem2  21680  xkoptsub  21692  xkopt  21693  qtopval  21733  qtopeu  21754  hmphindis  21835  txswaphmeolem  21842  ptuncnv  21845  ptunhmeo  21846  xpstopnlem1  21847  flimval  22001  fcfval  22071  alexsubALTlem3  22087  ptcmplem1  22090  ptcmplem2  22091  ptcmplem3  22092  ptcmplem4  22093  ptcmpg  22095  cnextfres1  22106  cldsubg  22148  utopval  22270  tusval  22304  tuslem  22305  tususs  22308  ucnval  22315  prdsxmslem2  22568  ishtpy  23005  pi1buni  23073  pi1xfrcnv  23090  elovolmr  23480  ovoliunlem3  23508  uniioombllem2  23587  uniioombllem3  23589  dyadmbl  23604  vmaval  25076  vmappw  25079  disjabrex  29743  disjabrexf  29744  fcnvgreu  29822  xrge0tsmseq  30135  locfinreflem  30255  locfinref  30256  pstmval  30286  pstmfval  30287  ordtprsuni  30313  esumeq12dvaf  30441  esumeq2  30446  esumval  30456  esumf1o  30460  esumsnf  30474  esumss  30482  esumpfinval  30485  esumpfinvalf  30486  sigapildsys  30573  sxsigon  30603  meascnbl  30630  brae  30652  braew  30653  faeval  30657  imambfm  30672  cnmbfm  30673  dya2iocuni  30693  omsval  30703  omsfval  30704  omsf  30706  oms0  30707  omssubaddlem  30709  omssubadd  30710  carsgval  30713  carsgclctunlem3  30730  omsmeas  30733  elprob  30819  probfinmeasb  30839  probmeasb  30840  dstrvprob  30881  indispconn  31561  iscvm  31586  cvmscld  31600  msrfval  31779  msrval  31780  mthmpps  31824  rdgprc0  32041  rdgprc  32042  dfrdg2  32043  dfrdg3  32044  trpredeq1  32062  trpredeq2  32063  trpredeq3  32064  frecseq123  32120  madeval  32278  unisnif  32375  brapply  32388  isfne  32677  fnemeet2  32705  fnejoin2  32707  tailfval  32710  ordcmp  32785  csbwrecsg  33509  mptsnunlem  33521  dissneqlem  33523  ptrest  33740  mblfinlem2  33779  ovoliunnfl  33783  voliunnfl  33785  volsupnfl  33786  nfunidALT2  34768  nfunidALT  34769  mapdunirnN  37449  aomclem8  38150  dfac21  38155  restuni6  39815  stoweidlem39  40753  salgenuni  41052  caragenval  41207  isome  41208  omeiunle  41231  isomennd  41245  unidmovn  41327  rrnmbl  41328  unidmvon  41331  hspmbl  41343  ovolval4lem2  41364  ovolval5lem2  41367  ovolval5lem3  41368  ovolval5  41369  ovnovollem2  41371  afv2eq12d  41822  setrecseq  43018