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 18	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  unisn3  4888  csbuni  4898  unisn2  5266  opswap  6220  unixpid  6277  iotaeq  6496  iotabi  6497  uniabio  6498  iotanul  6508  funfv  6961  funfv2  6962  fvun  6964  dffv2  6969  fniunfv  7240  ordunisuc  7827  orduniss2  7828  onsucuni2  7829  elxp4  7918  elxp5  7919  1stval  7987  2ndval  7988  1stnpr  7989  2ndnpr  7990  fo1st  8005  fo2nd  8006  f1stres  8009  f2ndres  8010  1st2val  8013  2nd2val  8014  2nd1st  8033  cnvf1olem  8105  brtpos2  8228  dftpos4  8241  tpostpos  8242  frecseq123  8279  csbfrecsg  8281  tz7.44-2  8394  tz7.44-3  8395  rdglim2  8419  ixpsnf1o  8945  xpcomco  9065  xpassen  9069  xpdom2  9070  supeq1  9415  supeq2  9418  supeq3  9419  supeq123d  9420  supval2  9425  rankuni  9849  en2other2  10045  dfac2a  10165  dfac12lem1  10179  dfac12r  10182  kmlem9  10194  kmlem11  10196  kmlem12  10197  enfin2i  10356  fin23lem29  10376  fin23lem30  10377  fin23lem32  10379  fin23lem34  10381  fin23lem35  10382  fin23lem36  10383  fin23lem38  10384  fin23lem39  10385  fin23lem41  10387  isf34lem7  10414  isf34lem6  10415  fin1a2lem10  10444  fin1a2lem11  10445  fin1a2lem12  10446  itunisuc  10454  itunitc  10456  ttukeylem3  10546  ttukey2g  10551  pwcfsdom  10625  gruurn  10840  dfinfre  12253  relexpfld  15155  relexpfldd  15156  fsumcnv  15892  fprodcnv  16103  mrcun  17743  isacs1i  17778  mreacs  17779  arwval  18165  ipoval  18651  isacs5lem  18666  acsdrscl  18667  acsficl  18668  isps  18689  isdir  18719  qustrivr  19344  ghmqusnsglem1  19441  ghmquskerlem1  19444  ghmquskerco  19445  gicqusker  19449  pmtrval  19612  pmtrfv  19613  pmtrprfv  19614  pmtrdifellem3  19639  pmtrprfval  19648  gsumcom2  20136  dmdprd  20161  dprddisj  20172  dprdf1o  20195  dprdsn  20199  dprd2da  20205  dprd2db  20206  dmdprdsplit2lem  20208  lspuni0  21232  lss0v  21238  zrhval  21760  zrhval2  21761  zrhpropd  21767  isbasisg  23212  basis1  23215  baspartn  23219  tgval  23220  eltg  23222  ntrfval  23289  ntrval  23301  tgrest  23424  restuni2  23432  lmfval  23497  cnfval  23498  cnpfval  23499  pnrmopn  23608  fiuncmp  23669  cmpfi  23673  ptval  23836  ptpjpre1  23837  elptr2  23840  ptuni2  23842  ptbasin  23843  ptbasfi  23847  xkoval  23853  txtopon  23857  ptuni  23860  ptunimpt  23861  xkouni  23865  ptpjcn  23877  ptcld  23879  dfac14  23884  ptcnp  23888  prdstopn  23894  ptrescn  23905  txcmplem2  23908  xkoptsub  23920  xkopt  23921  qtopval  23961  qtopeu  23982  hmphindis  24063  txswaphmeolem  24070  ptuncnv  24073  ptunhmeo  24074  xpstopnlem1  24075  flimval  24229  fcfval  24299  alexsubALTlem3  24315  ptcmplem1  24318  ptcmplem2  24319  ptcmplem3  24320  ptcmplem4  24321  ptcmpg  24323  cnextfres1  24334  cldsubg  24377  utopval  24498  tusval  24531  tuslem  24532  tususs  24535  ucnval  24542  prdsxmslem2  24795  ishtpy  25240  pi1buni  25308  pi1xfrcnv  25325  elovolmr  25744  ovoliunlem3  25772  uniioombllem2  25851  uniioombllem3  25853  dyadmbl  25868  vmaval  27389  vmappw  27392  madeval  28137  oldval  28139  madeoldsuc  28190  unidifsnel  33050  unidifsnne  33051  disjabrex  33095  disjabrexf  33096  fnpreimac  33183  fcnvgreu  33185  xrge0tsmseq  33555  cycpm2tr  33599  lmicqusker  33888  ricqusker  33896  esplyfval1  34124  dimval  34152  dimvalfi  34153  algextdeglem4  34271  algextdeg  34276  locfinreflem  34391  locfinref  34392  pstmval  34446  pstmfval  34447  ordtprsuni  34470  esumeq12dvaf  34582  esumeq2  34587  esumval  34597  esumf1o  34601  esumsnf  34615  esumss  34623  esumpfinval  34626  esumpfinvalf  34627  sigapildsys  34714  sxsigon  34744  meascnbl  34771  brae  34793  braew  34794  faeval  34798  imambfm  34814  cnmbfm  34815  dya2iocuni  34835  omsval  34845  omsfval  34846  omsf  34848  oms0  34849  omssubaddlem  34851  omssubadd  34852  carsgval  34855  carsgclctunlem3  34872  omsmeas  34875  elprob  34961  probfinmeasb  34980  probmeasb  34982  dstrvprob  35024  fineqvnttrclselem1  35708  fineqvnttrclselem2  35709  fineqvnttrclselem3  35710  fineqvnttrclse  35711  fineqvr1ombregs  35725  wevgblacfn  35809  indispconn  35914  iscvm  35939  cvmscld  35953  msrfval  36217  msrval  36218  mthmpps  36262  rdgprc0  36471  rdgprc  36472  dfrdg2  36473  dfrdg3  36474  unisnif  36603  brapply  36616  cbviotadavw  36974  isfne  37043  fnemeet2  37071  fnejoin2  37073  tailfval  37076  ordcmp  37151  ttcid  37196  bj-imafv  38086  mptsnunlem  38175  dissneqlem  38177  ctbssinf  38243  ptrest  38451  mblfinlem2  38490  ovoliunnfl  38494  voliunnfl  38496  volsupnfl  38497  nfunidALT2  39940  nfunidALT  39941  mapdunirnN  42621  zndvdchrrhm  42937  aks6d1c7lem2  43145  aks5lem4a  43154  prjcrvfval  43575  aomclem8  44000  dfac21  44005  rp-unirabeq  44161  rp-tfslim  44292  oaun2  44320  oaun3  44321  ismnu  45183  mnuprdlem1  45194  mnuprdlem2  45195  grumnudlem  45207  grumnud  45208  ismnushort  45223  restuni6  46052  stoweidlem39  46965  salgenuni  47263  caragenval  47419  isome  47420  omeiunle  47443  isomennd  47457  unidmovn  47539  rrnmbl  47540  unidmvon  47543  hspmbl  47555  ovolval4lem2  47576  ovolval5lem2  47579  ovolval5lem3  47580  ovolval5  47581  ovnovollem2  47583  tmachlem-tpopen  47867  tmachlem-uassst  47869  afv2eq12d  48201  uniimaelsetpreimafv  48394  fundcmpsurinjlem3  48398  imasetpreimafvbijlemfo  48403  fundcmpsurbijinjpreimafv  48405  dftpos5  49898  tposideq  49912  restcls2lem  49937  mreclat  50021  toplatglb  50025  swapf1a  50293  swapf2a  50295  swapf1  50296  swapf2  50298  setrecseq  50704