Theorem unieqd 4869

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  unisn3  4877  csbuni  4886  unisn2  5248  opswap  6176  unixpid  6231  iotaeq  6449  iotabi  6450  uniabio  6451  iotanul  6461  funfv  6909  funfv2  6910  fvun  6912  dffv2  6917  fniunfv  7181  ordunisuc  7762  orduniss2  7763  onsucuni2  7764  elxp4  7852  elxp5  7853  1stval  7923  2ndval  7924  1stnpr  7925  2ndnpr  7926  fo1st  7941  fo2nd  7942  f1stres  7945  f2ndres  7946  1st2val  7949  2nd2val  7950  2nd1st  7970  cnvf1olem  8040  brtpos2  8162  dftpos4  8175  tpostpos  8176  frecseq123  8212  csbfrecsg  8214  tz7.44-2  8326  tz7.44-3  8327  rdglim2  8351  ixpsnf1o  8862  xpcomco  8980  xpassen  8984  xpdom2  8985  supeq1  9329  supeq2  9332  supeq3  9333  supeq123d  9334  supval2  9339  rankuni  9756  en2other2  9900  dfac2a  10021  dfac12lem1  10035  dfac12r  10038  kmlem9  10050  kmlem11  10052  kmlem12  10053  enfin2i  10212  fin23lem29  10232  fin23lem30  10233  fin23lem32  10235  fin23lem34  10237  fin23lem35  10238  fin23lem36  10239  fin23lem38  10240  fin23lem39  10241  fin23lem41  10243  isf34lem7  10270  isf34lem6  10271  fin1a2lem10  10300  fin1a2lem11  10301  fin1a2lem12  10302  itunisuc  10310  itunitc  10312  ttukeylem3  10402  ttukey2g  10407  pwcfsdom  10474  gruurn  10689  dfinfre  12103  relexpfld  14956  relexpfldd  14957  fsumcnv  15680  fprodcnv  15890  mrcun  17528  isacs1i  17563  mreacs  17564  arwval  17950  ipoval  18436  isacs5lem  18451  acsdrscl  18452  acsficl  18453  isps  18474  isdir  18504  ghmqusnsglem1  19192  ghmquskerlem1  19195  ghmquskerco  19196  gicqusker  19200  pmtrval  19363  pmtrfv  19364  pmtrprfv  19365  pmtrdifellem3  19390  pmtrprfval  19399  gsumcom2  19887  dmdprd  19912  dprddisj  19923  dprdf1o  19946  dprdsn  19950  dprd2da  19956  dprd2db  19957  dmdprdsplit2lem  19959  lspuni0  20943  lss0v  20950  zrhval  21444  zrhval2  21445  zrhpropd  21451  isbasisg  22862  basis1  22865  baspartn  22869  tgval  22870  eltg  22872  ntrfval  22939  ntrval  22951  tgrest  23074  restuni2  23082  lmfval  23147  cnfval  23148  cnpfval  23149  pnrmopn  23258  fiuncmp  23319  cmpfi  23323  ptval  23485  ptpjpre1  23486  elptr2  23489  ptuni2  23491  ptbasin  23492  ptbasfi  23496  xkoval  23502  txtopon  23506  ptuni  23509  ptunimpt  23510  xkouni  23514  ptpjcn  23526  ptcld  23528  dfac14  23533  ptcnp  23537  prdstopn  23543  ptrescn  23554  txcmplem2  23557  xkoptsub  23569  xkopt  23570  qtopval  23610  qtopeu  23631  hmphindis  23712  txswaphmeolem  23719  ptuncnv  23722  ptunhmeo  23723  xpstopnlem1  23724  flimval  23878  fcfval  23948  alexsubALTlem3  23964  ptcmplem1  23967  ptcmplem2  23968  ptcmplem3  23969  ptcmplem4  23970  ptcmpg  23972  cnextfres1  23983  cldsubg  24026  utopval  24147  tusval  24180  tuslem  24181  tususs  24184  ucnval  24191  prdsxmslem2  24444  ishtpy  24898  pi1buni  24967  pi1xfrcnv  24984  elovolmr  25404  ovoliunlem3  25432  uniioombllem2  25511  uniioombllem3  25513  dyadmbl  25528  vmaval  27050  vmappw  27053  madeval  27793  oldval  27795  madeoldsuc  27830  zs12bday  28394  unidifsnel  32515  unidifsnne  32516  disjabrex  32562  disjabrexf  32563  fnpreimac  32653  fcnvgreu  32655  xrge0tsmseq  33044  cycpm2tr  33088  qustrivr  33330  lmicqusker  33383  ricqusker  33392  dimval  33613  dimvalfi  33614  algextdeglem4  33733  algextdeg  33738  locfinreflem  33853  locfinref  33854  pstmval  33908  pstmfval  33909  ordtprsuni  33932  esumeq12dvaf  34044  esumeq2  34049  esumval  34059  esumf1o  34063  esumsnf  34077  esumss  34085  esumpfinval  34088  esumpfinvalf  34089  sigapildsys  34175  sxsigon  34205  meascnbl  34232  brae  34254  braew  34255  faeval  34259  imambfm  34275  cnmbfm  34276  dya2iocuni  34296  omsval  34306  omsfval  34307  omsf  34309  oms0  34310  omssubaddlem  34312  omssubadd  34313  carsgval  34316  carsgclctunlem3  34333  omsmeas  34336  elprob  34422  probfinmeasb  34441  probmeasb  34443  dstrvprob  34485  fineqvr1ombregs  35135  fineqvnttrclselem1  35141  fineqvnttrclselem2  35142  fineqvnttrclselem3  35143  fineqvnttrclse  35144  wevgblacfn  35153  indispconn  35278  iscvm  35303  cvmscld  35317  msrfval  35581  msrval  35582  mthmpps  35626  rdgprc0  35835  rdgprc  35836  dfrdg2  35837  dfrdg3  35838  unisnif  35967  brapply  35980  cbviotadavw  36313  isfne  36383  fnemeet2  36411  fnejoin2  36413  tailfval  36416  ordcmp  36491  bj-imafv  37295  mptsnunlem  37382  dissneqlem  37384  ctbssinf  37450  ptrest  37658  mblfinlem2  37697  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  nfunidALT2  39067  nfunidALT  39068  mapdunirnN  41748  zndvdchrrhm  42064  aks6d1c7lem2  42273  aks5lem4a  42282  prjcrvfval  42723  aomclem8  43153  dfac21  43158  rp-unirabeq  43314  rp-tfslim  43445  oaun2  43473  oaun3  43474  ismnu  44353  mnuprdlem1  44364  mnuprdlem2  44365  grumnudlem  44377  grumnud  44378  ismnushort  44393  restuni6  45218  stoweidlem39  46136  salgenuni  46434  caragenval  46590  isome  46591  omeiunle  46614  isomennd  46628  unidmovn  46710  rrnmbl  46711  unidmvon  46714  hspmbl  46726  ovolval4lem2  46747  ovolval5lem2  46750  ovolval5lem3  46751  ovolval5  46752  ovnovollem2  46754  afv2eq12d  47314  uniimaelsetpreimafv  47495  fundcmpsurinjlem3  47499  imasetpreimafvbijlemfo  47504  fundcmpsurbijinjpreimafv  47506  dftpos5  48973  tposideq  48987  restcls2lem  49012  mreclat  49096  toplatglb  49100  swapf1a  49369  swapf2a  49371  swapf1  49372  swapf2  49374  setrecseq  49785