Theorem unieqd 4878

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

Syntax hints:   → wi 4   = wceq 1542  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unisn3  4886  csbuni  4895  unisn2  5261  opswap  6197  unixpid  6252  iotaeq  6470  iotabi  6471  uniabio  6472  iotanul  6482  funfv  6931  funfv2  6932  fvun  6934  dffv2  6939  fniunfv  7205  ordunisuc  7786  orduniss2  7787  onsucuni2  7788  elxp4  7876  elxp5  7877  1stval  7947  2ndval  7948  1stnpr  7949  2ndnpr  7950  fo1st  7965  fo2nd  7966  f1stres  7969  f2ndres  7970  1st2val  7973  2nd2val  7974  2nd1st  7994  cnvf1olem  8064  brtpos2  8186  dftpos4  8199  tpostpos  8200  frecseq123  8236  csbfrecsg  8238  tz7.44-2  8350  tz7.44-3  8351  rdglim2  8375  ixpsnf1o  8890  xpcomco  9009  xpassen  9013  xpdom2  9014  supeq1  9362  supeq2  9365  supeq3  9366  supeq123d  9367  supval2  9372  rankuni  9789  en2other2  9933  dfac2a  10054  dfac12lem1  10068  dfac12r  10071  kmlem9  10083  kmlem11  10085  kmlem12  10086  enfin2i  10245  fin23lem29  10265  fin23lem30  10266  fin23lem32  10268  fin23lem34  10270  fin23lem35  10271  fin23lem36  10272  fin23lem38  10273  fin23lem39  10274  fin23lem41  10276  isf34lem7  10303  isf34lem6  10304  fin1a2lem10  10333  fin1a2lem11  10334  fin1a2lem12  10335  itunisuc  10343  itunitc  10345  ttukeylem3  10435  ttukey2g  10440  pwcfsdom  10508  gruurn  10723  dfinfre  12137  relexpfld  14986  relexpfldd  14987  fsumcnv  15710  fprodcnv  15920  mrcun  17559  isacs1i  17594  mreacs  17595  arwval  17981  ipoval  18467  isacs5lem  18482  acsdrscl  18483  acsficl  18484  isps  18505  isdir  18535  ghmqusnsglem1  19226  ghmquskerlem1  19229  ghmquskerco  19230  gicqusker  19234  pmtrval  19397  pmtrfv  19398  pmtrprfv  19399  pmtrdifellem3  19424  pmtrprfval  19433  gsumcom2  19921  dmdprd  19946  dprddisj  19957  dprdf1o  19980  dprdsn  19984  dprd2da  19990  dprd2db  19991  dmdprdsplit2lem  19993  lspuni0  20978  lss0v  20985  zrhval  21479  zrhval2  21480  zrhpropd  21486  isbasisg  22908  basis1  22911  baspartn  22915  tgval  22916  eltg  22918  ntrfval  22985  ntrval  22997  tgrest  23120  restuni2  23128  lmfval  23193  cnfval  23194  cnpfval  23195  pnrmopn  23304  fiuncmp  23365  cmpfi  23369  ptval  23531  ptpjpre1  23532  elptr2  23535  ptuni2  23537  ptbasin  23538  ptbasfi  23542  xkoval  23548  txtopon  23552  ptuni  23555  ptunimpt  23556  xkouni  23560  ptpjcn  23572  ptcld  23574  dfac14  23579  ptcnp  23583  prdstopn  23589  ptrescn  23600  txcmplem2  23603  xkoptsub  23615  xkopt  23616  qtopval  23656  qtopeu  23677  hmphindis  23758  txswaphmeolem  23765  ptuncnv  23768  ptunhmeo  23769  xpstopnlem1  23770  flimval  23924  fcfval  23994  alexsubALTlem3  24010  ptcmplem1  24013  ptcmplem2  24014  ptcmplem3  24015  ptcmplem4  24016  ptcmpg  24018  cnextfres1  24029  cldsubg  24072  utopval  24193  tusval  24226  tuslem  24227  tususs  24230  ucnval  24237  prdsxmslem2  24490  ishtpy  24944  pi1buni  25013  pi1xfrcnv  25030  elovolmr  25450  ovoliunlem3  25478  uniioombllem2  25557  uniioombllem3  25559  dyadmbl  25574  vmaval  27096  vmappw  27099  madeval  27845  oldval  27847  madeoldsuc  27898  unidifsnel  32628  unidifsnne  32629  disjabrex  32675  disjabrexf  32676  fnpreimac  32766  fcnvgreu  32768  xrge0tsmseq  33175  cycpm2tr  33219  qustrivr  33464  lmicqusker  33517  ricqusker  33526  esplyfval1  33756  dimval  33784  dimvalfi  33785  algextdeglem4  33904  algextdeg  33909  locfinreflem  34024  locfinref  34025  pstmval  34079  pstmfval  34080  ordtprsuni  34103  esumeq12dvaf  34215  esumeq2  34220  esumval  34230  esumf1o  34234  esumsnf  34248  esumss  34256  esumpfinval  34259  esumpfinvalf  34260  sigapildsys  34346  sxsigon  34376  meascnbl  34403  brae  34425  braew  34426  faeval  34430  imambfm  34446  cnmbfm  34447  dya2iocuni  34467  omsval  34477  omsfval  34478  omsf  34480  oms0  34481  omssubaddlem  34483  omssubadd  34484  carsgval  34487  carsgclctunlem3  34504  omsmeas  34507  elprob  34593  probfinmeasb  34612  probmeasb  34614  dstrvprob  34656  fineqvnttrclselem1  35305  fineqvnttrclselem2  35306  fineqvnttrclselem3  35307  fineqvnttrclse  35308  fineqvr1ombregs  35322  wevgblacfn  35331  indispconn  35456  iscvm  35481  cvmscld  35495  msrfval  35759  msrval  35760  mthmpps  35804  rdgprc0  36013  rdgprc  36014  dfrdg2  36015  dfrdg3  36016  unisnif  36145  brapply  36158  cbviotadavw  36491  isfne  36561  fnemeet2  36589  fnejoin2  36591  tailfval  36594  ordcmp  36669  bj-imafv  37533  mptsnunlem  37620  dissneqlem  37622  ctbssinf  37688  ptrest  37899  mblfinlem2  37938  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  nfunidALT2  39374  nfunidALT  39375  mapdunirnN  42055  zndvdchrrhm  42371  aks6d1c7lem2  42580  aks5lem4a  42589  prjcrvfval  43018  aomclem8  43447  dfac21  43452  rp-unirabeq  43608  rp-tfslim  43739  oaun2  43767  oaun3  43768  ismnu  44646  mnuprdlem1  44657  mnuprdlem2  44658  grumnudlem  44670  grumnud  44671  ismnushort  44686  restuni6  45510  stoweidlem39  46426  salgenuni  46724  caragenval  46880  isome  46881  omeiunle  46904  isomennd  46918  unidmovn  47000  rrnmbl  47001  unidmvon  47004  hspmbl  47016  ovolval4lem2  47037  ovolval5lem2  47040  ovolval5lem3  47041  ovolval5  47042  ovnovollem2  47044  afv2eq12d  47604  uniimaelsetpreimafv  47785  fundcmpsurinjlem3  47789  imasetpreimafvbijlemfo  47794  fundcmpsurbijinjpreimafv  47796  dftpos5  49262  tposideq  49276  restcls2lem  49301  mreclat  49385  toplatglb  49389  swapf1a  49657  swapf2a  49659  swapf1  49660  swapf2  49662  setrecseq  50073