Theorem unieqd 4382

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

Syntax hints:   → wi 4   = wceq 1475  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373

This theorem is referenced by:  uniprg  4386  unisng  4388  unisn3  4389  csbuni  4402  unisn2  4722  opswap  5540  unixpid  5587  iotaeq  5776  iotabi  5777  uniabio  5778  iotanul  5783  funfv  6175  funfv2  6176  fvun  6178  dffv2  6181  fniunfv  6409  ordunisuc  6924  orduniss2  6925  onsucuni2  6926  elxp4  7003  elxp5  7004  1stval  7061  2ndval  7062  1stnpr  7063  2ndnpr  7064  fo1st  7079  fo2nd  7080  f1stres  7081  f2ndres  7082  1st2val  7085  2nd2val  7086  2nd1st  7104  cnvf1olem  7162  brtpos2  7245  dftpos4  7258  tpostpos  7259  wrecseq123  7295  tz7.44-2  7390  tz7.44-3  7391  rdglim2  7415  ixpsnf1o  7834  xpcomco  7935  xpassen  7939  xpdom2  7940  supeq1  8234  supeq2  8237  supeq3  8238  supeq123d  8239  supval2  8244  rankuni  8609  en2other2  8715  dfac2a  8835  dfac12lem1  8848  dfac12r  8851  kmlem9  8863  kmlem11  8865  kmlem12  8866  enfin2i  9026  fin23lem29  9046  fin23lem30  9047  fin23lem32  9049  fin23lem34  9051  fin23lem35  9052  fin23lem36  9053  fin23lem38  9054  fin23lem39  9055  fin23lem41  9057  isf34lem7  9084  isf34lem6  9085  fin1a2lem10  9114  fin1a2lem11  9115  fin1a2lem12  9116  itunisuc  9124  itunitc  9126  ttukeylem3  9216  ttukey2g  9221  pwcfsdom  9284  gruurn  9499  dfinfre  10881  relexpfld  13637  fsumcnv  14346  fprodcnv  14552  mrcun  16105  isacs1i  16141  mreacs  16142  arwval  16516  ipoval  16977  isacs5lem  16992  acsdrscl  16993  acsficl  16994  isps  17025  isdir  17055  pmtrval  17694  pmtrfv  17695  pmtrprfv  17696  pmtrdifellem3  17721  pmtrprfval  17730  gsumcom2  18197  dmdprd  18220  dprddisj  18231  dprdf1o  18254  dprdsn  18258  dprd2da  18264  dprd2db  18265  dmdprdsplit2lem  18267  lspuni0  18831  lss0v  18837  zrhval  19675  zrhval2  19676  zrhpropd  19682  isbasisg  20562  basis1  20565  baspartn  20569  tgval  20570  eltg  20572  ntrfval  20638  ntrval  20650  tgrest  20773  restuni2  20781  lmfval  20846  cnfval  20847  cnpfval  20848  pnrmopn  20957  fiuncmp  21017  cmpfi  21021  ptval  21183  ptpjpre1  21184  elptr2  21187  ptuni2  21189  ptbasin  21190  ptbasfi  21194  xkoval  21200  txtopon  21204  ptuni  21207  ptunimpt  21208  xkouni  21212  ptpjcn  21224  ptcld  21226  dfac14  21231  ptcnp  21235  prdstopn  21241  ptrescn  21252  txcmplem2  21255  xkoptsub  21267  xkopt  21268  qtopval  21308  qtopeu  21329  hmphindis  21410  txswaphmeolem  21417  ptuncnv  21420  ptunhmeo  21421  xpstopnlem1  21422  flimval  21577  fcfval  21647  alexsubALTlem3  21663  ptcmplem1  21666  ptcmplem2  21667  ptcmplem3  21668  ptcmplem4  21669  ptcmpg  21671  cnextfres1  21682  cldsubg  21724  utopval  21846  tusval  21880  tuslem  21881  tususs  21884  ucnval  21891  prdsxmslem2  22144  ishtpy  22579  pi1buni  22648  pi1xfrcnv  22665  elovolmr  23051  ovoliunlem3  23079  uniioombllem2  23157  uniioombllem3  23159  dyadmbl  23174  vmaval  24639  vmappw  24642  disjabrex  28777  disjabrexf  28778  fcnvgreu  28855  xrge0tsmseq  29118  locfinreflem  29235  locfinref  29236  pstmval  29266  pstmfval  29267  ordtprsuni  29293  esumeq12dvaf  29420  esumeq2  29425  esumval  29435  esumf1o  29439  esumsnf  29453  esumss  29461  esumpfinval  29464  esumpfinvalf  29465  sigapildsys  29552  sxsigon  29582  meascnbl  29609  brae  29631  braew  29632  faeval  29636  imambfm  29651  cnmbfm  29652  dya2iocuni  29672  omsval  29682  omsfval  29683  omsf  29685  oms0  29686  omssubaddlem  29688  omssubadd  29689  carsgval  29692  carsgclctunlem3  29709  omsmeas  29712  elprob  29798  probfinmeasb  29818  probmeasb  29819  dstrvprob  29860  indispcon  30470  iscvm  30495  cvmscld  30509  msrfval  30688  msrval  30689  mthmpps  30733  rdgprc0  30943  rdgprc  30944  dfrdg2  30945  dfrdg3  30946  trpredeq1  30964  trpredeq2  30965  trpredeq3  30966  nofulllem1  31101  nofulllem2  31102  unisnif  31202  brapply  31215  isfne  31504  fnemeet2  31532  fnejoin2  31534  tailfval  31537  ordcmp  31616  csbwrecsg  32349  mptsnunlem  32361  dissneqlem  32363  ptrest  32578  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  nfunidALT2  33274  nfunidALT  33275  mapdunirnN  35957  aomclem8  36649  dfac21  36654  csbfv12gALTOLD  38074  restuni6  38337  stoweidlem39  38932  salgenuni  39231  caragenval  39383  isome  39384  omeiunle  39407  isomennd  39421  unidmovn  39503  rrnmbl  39504  unidmvon  39507  hspmbl  39519  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovollem2  39547  setrecseq  42231