Theorem unieqd 4880

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

Syntax hints:   → wi 4   = wceq 1540  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868

This theorem is referenced by:  unisn3  4888  csbuni  4896  unisn2  5262  opswap  6190  unixpid  6245  iotaeq  6464  iotabi  6465  uniabio  6466  iotanul  6477  funfv  6930  funfv2  6931  fvun  6933  dffv2  6938  fniunfv  7203  ordunisuc  7787  orduniss2  7788  onsucuni2  7789  elxp4  7878  elxp5  7879  1stval  7949  2ndval  7950  1stnpr  7951  2ndnpr  7952  fo1st  7967  fo2nd  7968  f1stres  7971  f2ndres  7972  1st2val  7975  2nd2val  7976  2nd1st  7996  cnvf1olem  8066  brtpos2  8188  dftpos4  8201  tpostpos  8202  frecseq123  8238  csbfrecsg  8240  tz7.44-2  8352  tz7.44-3  8353  rdglim2  8377  ixpsnf1o  8888  xpcomco  9008  xpassen  9012  xpdom2  9013  supeq1  9372  supeq2  9375  supeq3  9376  supeq123d  9377  supval2  9382  rankuni  9792  en2other2  9938  dfac2a  10059  dfac12lem1  10073  dfac12r  10076  kmlem9  10088  kmlem11  10090  kmlem12  10091  enfin2i  10250  fin23lem29  10270  fin23lem30  10271  fin23lem32  10273  fin23lem34  10275  fin23lem35  10276  fin23lem36  10277  fin23lem38  10278  fin23lem39  10279  fin23lem41  10281  isf34lem7  10308  isf34lem6  10309  fin1a2lem10  10338  fin1a2lem11  10339  fin1a2lem12  10340  itunisuc  10348  itunitc  10350  ttukeylem3  10440  ttukey2g  10445  pwcfsdom  10512  gruurn  10727  dfinfre  12140  relexpfld  14991  relexpfldd  14992  fsumcnv  15715  fprodcnv  15925  mrcun  17563  isacs1i  17598  mreacs  17599  arwval  17985  ipoval  18471  isacs5lem  18486  acsdrscl  18487  acsficl  18488  isps  18509  isdir  18539  ghmqusnsglem1  19194  ghmquskerlem1  19197  ghmquskerco  19198  gicqusker  19202  pmtrval  19365  pmtrfv  19366  pmtrprfv  19367  pmtrdifellem3  19392  pmtrprfval  19401  gsumcom2  19889  dmdprd  19914  dprddisj  19925  dprdf1o  19948  dprdsn  19952  dprd2da  19958  dprd2db  19959  dmdprdsplit2lem  19961  lspuni0  20948  lss0v  20955  zrhval  21449  zrhval2  21450  zrhpropd  21456  isbasisg  22867  basis1  22870  baspartn  22874  tgval  22875  eltg  22877  ntrfval  22944  ntrval  22956  tgrest  23079  restuni2  23087  lmfval  23152  cnfval  23153  cnpfval  23154  pnrmopn  23263  fiuncmp  23324  cmpfi  23328  ptval  23490  ptpjpre1  23491  elptr2  23494  ptuni2  23496  ptbasin  23497  ptbasfi  23501  xkoval  23507  txtopon  23511  ptuni  23514  ptunimpt  23515  xkouni  23519  ptpjcn  23531  ptcld  23533  dfac14  23538  ptcnp  23542  prdstopn  23548  ptrescn  23559  txcmplem2  23562  xkoptsub  23574  xkopt  23575  qtopval  23615  qtopeu  23636  hmphindis  23717  txswaphmeolem  23724  ptuncnv  23727  ptunhmeo  23728  xpstopnlem1  23729  flimval  23883  fcfval  23953  alexsubALTlem3  23969  ptcmplem1  23972  ptcmplem2  23973  ptcmplem3  23974  ptcmplem4  23975  ptcmpg  23977  cnextfres1  23988  cldsubg  24031  utopval  24153  tusval  24186  tuslem  24187  tususs  24190  ucnval  24197  prdsxmslem2  24450  ishtpy  24904  pi1buni  24973  pi1xfrcnv  24990  elovolmr  25410  ovoliunlem3  25438  uniioombllem2  25517  uniioombllem3  25519  dyadmbl  25534  vmaval  27056  vmappw  27059  madeval  27797  oldval  27799  madeoldsuc  27834  zs12bday  28396  unidifsnel  32514  unidifsnne  32515  disjabrex  32561  disjabrexf  32562  fnpreimac  32645  fcnvgreu  32647  xrge0tsmseq  33047  cycpm2tr  33091  qustrivr  33329  lmicqusker  33382  ricqusker  33391  dimval  33589  dimvalfi  33590  algextdeglem4  33703  algextdeg  33708  locfinreflem  33823  locfinref  33824  pstmval  33878  pstmfval  33879  ordtprsuni  33902  esumeq12dvaf  34014  esumeq2  34019  esumval  34029  esumf1o  34033  esumsnf  34047  esumss  34055  esumpfinval  34058  esumpfinvalf  34059  sigapildsys  34145  sxsigon  34175  meascnbl  34202  brae  34224  braew  34225  faeval  34229  imambfm  34246  cnmbfm  34247  dya2iocuni  34267  omsval  34277  omsfval  34278  omsf  34280  oms0  34281  omssubaddlem  34283  omssubadd  34284  carsgval  34287  carsgclctunlem3  34304  omsmeas  34307  elprob  34393  probfinmeasb  34412  probmeasb  34414  dstrvprob  34456  wevgblacfn  35089  indispconn  35214  iscvm  35239  cvmscld  35253  msrfval  35517  msrval  35518  mthmpps  35562  rdgprc0  35774  rdgprc  35775  dfrdg2  35776  dfrdg3  35777  unisnif  35906  brapply  35919  cbviotadavw  36250  isfne  36320  fnemeet2  36348  fnejoin2  36350  tailfval  36353  ordcmp  36428  bj-imafv  37232  mptsnunlem  37319  dissneqlem  37321  ctbssinf  37387  ptrest  37606  mblfinlem2  37645  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  nfunidALT2  38955  nfunidALT  38956  mapdunirnN  41637  zndvdchrrhm  41953  aks6d1c7lem2  42162  aks5lem4a  42171  prjcrvfval  42612  aomclem8  43043  dfac21  43048  rp-unirabeq  43204  rp-tfslim  43335  oaun2  43363  oaun3  43364  ismnu  44243  mnuprdlem1  44254  mnuprdlem2  44255  grumnudlem  44267  grumnud  44268  ismnushort  44283  restuni6  45109  stoweidlem39  46030  salgenuni  46328  caragenval  46484  isome  46485  omeiunle  46508  isomennd  46522  unidmovn  46604  rrnmbl  46605  unidmvon  46608  hspmbl  46620  ovolval4lem2  46641  ovolval5lem2  46644  ovolval5lem3  46645  ovolval5  46646  ovnovollem2  46648  afv2eq12d  47209  uniimaelsetpreimafv  47390  fundcmpsurinjlem3  47394  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  dftpos5  48855  tposideq  48869  restcls2lem  48894  mreclat  48978  toplatglb  48982  swapf1a  49251  swapf2a  49253  swapf1  49254  swapf2  49256  setrecseq  49667