Theorem unieqd 4833

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

Syntax hints:   → wi 4   = wceq 1543  ∪ cuni 4819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820

This theorem is referenced by:  uniprgOLD  4839  unisn3  4842  csbuni  4850  unisn2  5205  opswap  6092  unixpid  6147  iotaeq  6351  iotabi  6352  uniabio  6353  iotanul  6358  funfv  6798  funfv2  6799  fvun  6801  dffv2  6806  fniunfv  7060  ordunisuc  7611  orduniss2  7612  onsucuni2  7613  elxp4  7700  elxp5  7701  1stval  7763  2ndval  7764  1stnpr  7765  2ndnpr  7766  fo1st  7781  fo2nd  7782  f1stres  7785  f2ndres  7786  1st2val  7789  2nd2val  7790  2nd1st  7809  cnvf1olem  7878  brtpos2  7974  dftpos4  7987  tpostpos  7988  frecseq123  8024  wrecseq123  8048  tz7.44-2  8143  tz7.44-3  8144  rdglim2  8168  ixpsnf1o  8619  xpcomco  8735  xpassen  8739  xpdom2  8740  supeq1  9061  supeq2  9064  supeq3  9065  supeq123d  9066  supval2  9071  trpredeq1  9325  trpredeq2  9326  trpredeq3  9327  rankuni  9479  en2other2  9623  dfac2a  9743  dfac12lem1  9757  dfac12r  9760  kmlem9  9772  kmlem11  9774  kmlem12  9775  enfin2i  9935  fin23lem29  9955  fin23lem30  9956  fin23lem32  9958  fin23lem34  9960  fin23lem35  9961  fin23lem36  9962  fin23lem38  9963  fin23lem39  9964  fin23lem41  9966  isf34lem7  9993  isf34lem6  9994  fin1a2lem10  10023  fin1a2lem11  10024  fin1a2lem12  10025  itunisuc  10033  itunitc  10035  ttukeylem3  10125  ttukey2g  10130  pwcfsdom  10197  gruurn  10412  dfinfre  11813  relexpfld  14612  relexpfldd  14613  fsumcnv  15337  fprodcnv  15545  mrcun  17125  isacs1i  17160  mreacs  17161  arwval  17549  ipoval  18036  isacs5lem  18051  acsdrscl  18052  acsficl  18053  isps  18074  isdir  18104  pmtrval  18843  pmtrfv  18844  pmtrprfv  18845  pmtrdifellem3  18870  pmtrprfval  18879  gsumcom2  19360  dmdprd  19385  dprddisj  19396  dprdf1o  19419  dprdsn  19423  dprd2da  19429  dprd2db  19430  dmdprdsplit2lem  19432  lspuni0  20047  lss0v  20053  zrhval  20474  zrhval2  20475  zrhpropd  20481  isbasisg  21844  basis1  21847  baspartn  21851  tgval  21852  eltg  21854  ntrfval  21921  ntrval  21933  tgrest  22056  restuni2  22064  lmfval  22129  cnfval  22130  cnpfval  22131  pnrmopn  22240  fiuncmp  22301  cmpfi  22305  ptval  22467  ptpjpre1  22468  elptr2  22471  ptuni2  22473  ptbasin  22474  ptbasfi  22478  xkoval  22484  txtopon  22488  ptuni  22491  ptunimpt  22492  xkouni  22496  ptpjcn  22508  ptcld  22510  dfac14  22515  ptcnp  22519  prdstopn  22525  ptrescn  22536  txcmplem2  22539  xkoptsub  22551  xkopt  22552  qtopval  22592  qtopeu  22613  hmphindis  22694  txswaphmeolem  22701  ptuncnv  22704  ptunhmeo  22705  xpstopnlem1  22706  flimval  22860  fcfval  22930  alexsubALTlem3  22946  ptcmplem1  22949  ptcmplem2  22950  ptcmplem3  22951  ptcmplem4  22952  ptcmpg  22954  cnextfres1  22965  cldsubg  23008  utopval  23130  tusval  23163  tuslem  23164  tususs  23167  ucnval  23174  prdsxmslem2  23427  ishtpy  23869  pi1buni  23937  pi1xfrcnv  23954  elovolmr  24373  ovoliunlem3  24401  uniioombllem2  24480  uniioombllem3  24482  dyadmbl  24497  vmaval  25995  vmappw  25998  unidifsnel  30602  unidifsnne  30603  disjabrex  30640  disjabrexf  30641  fnpreimac  30728  fcnvgreu  30730  xrge0tsmseq  31038  cycpm2tr  31105  qustrivr  31275  dimval  31400  dimvalfi  31401  locfinreflem  31504  locfinref  31505  pstmval  31559  pstmfval  31560  ordtprsuni  31583  esumeq12dvaf  31711  esumeq2  31716  esumval  31726  esumf1o  31730  esumsnf  31744  esumss  31752  esumpfinval  31755  esumpfinvalf  31756  sigapildsys  31842  sxsigon  31872  meascnbl  31899  brae  31921  braew  31922  faeval  31926  imambfm  31941  cnmbfm  31942  dya2iocuni  31962  omsval  31972  omsfval  31973  omsf  31975  oms0  31976  omssubaddlem  31978  omssubadd  31979  carsgval  31982  carsgclctunlem3  31999  omsmeas  32002  elprob  32088  probfinmeasb  32107  probmeasb  32109  dstrvprob  32150  indispconn  32909  iscvm  32934  cvmscld  32948  msrfval  33212  msrval  33213  mthmpps  33257  rdgprc0  33488  rdgprc  33489  dfrdg2  33490  dfrdg3  33491  madeval  33773  oldval  33775  madeoldsuc  33804  unisnif  33964  brapply  33977  isfne  34265  fnemeet2  34293  fnejoin2  34295  tailfval  34298  ordcmp  34373  bj-imafv  35157  csbwrecsg  35235  mptsnunlem  35246  dissneqlem  35248  ctbssinf  35314  ptrest  35513  mblfinlem2  35552  ovoliunnfl  35556  voliunnfl  35558  volsupnfl  35559  nfunidALT2  36720  nfunidALT  36721  mapdunirnN  39401  aomclem8  40589  dfac21  40594  ismnu  41552  mnuprdlem1  41563  mnuprdlem2  41564  grumnudlem  41576  grumnud  41577  ismnushort  41592  restuni6  42344  stoweidlem39  43255  salgenuni  43551  caragenval  43706  isome  43707  omeiunle  43730  isomennd  43744  unidmovn  43826  rrnmbl  43827  unidmvon  43830  hspmbl  43842  ovolval4lem2  43863  ovolval5lem2  43866  ovolval5lem3  43867  ovolval5  43868  ovnovollem2  43870  afv2eq12d  44379  uniimaelsetpreimafv  44521  fundcmpsurinjlem3  44525  imasetpreimafvbijlemfo  44530  fundcmpsurbijinjpreimafv  44532  restcls2lem  45879  mreclat  45956  toplatglb  45960  setrecseq  46062