Theorem unieqd 4883

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  unisn3  4891  csbuni  4901  unisn2  5273  opswap  6229  unixpid  6286  iotaeq  6505  iotabi  6506  uniabio  6507  iotanul  6517  funfv  6969  funfv2  6970  fvun  6972  dffv2  6977  fniunfv  7247  ordunisuc  7831  orduniss2  7832  onsucuni2  7833  elxp4  7922  elxp5  7923  1stval  7991  2ndval  7992  1stnpr  7993  2ndnpr  7994  fo1st  8009  fo2nd  8010  f1stres  8013  f2ndres  8014  1st2val  8017  2nd2val  8018  2nd1st  8038  cnvf1olem  8110  brtpos2  8233  dftpos4  8246  tpostpos  8247  frecseq123  8284  csbfrecsg  8286  tz7.44-2  8399  tz7.44-3  8400  rdglim2  8424  ixpsnf1o  8948  xpcomco  9068  xpassen  9072  xpdom2  9073  supeq1  9418  supeq2  9421  supeq3  9422  supeq123d  9423  supval2  9428  rankuni  9848  en2other2  10015  dfac2a  10135  dfac12lem1  10149  dfac12r  10152  kmlem9  10164  kmlem11  10166  kmlem12  10167  enfin2i  10326  fin23lem29  10346  fin23lem30  10347  fin23lem32  10349  fin23lem34  10351  fin23lem35  10352  fin23lem36  10353  fin23lem38  10354  fin23lem39  10355  fin23lem41  10357  isf34lem7  10384  isf34lem6  10385  fin1a2lem10  10414  fin1a2lem11  10415  fin1a2lem12  10416  itunisuc  10424  itunitc  10426  ttukeylem3  10516  ttukey2g  10521  pwcfsdom  10595  gruurn  10810  dfinfre  12223  relexpfld  15124  relexpfldd  15125  fsumcnv  15861  fprodcnv  16074  mrcun  17714  isacs1i  17749  mreacs  17750  arwval  18136  ipoval  18622  isacs5lem  18637  acsdrscl  18638  acsficl  18639  isps  18660  isdir  18690  qustrivr  19311  ghmqusnsglem1  19408  ghmquskerlem1  19411  ghmquskerco  19412  gicqusker  19416  pmtrval  19579  pmtrfv  19580  pmtrprfv  19581  pmtrdifellem3  19606  pmtrprfval  19615  gsumcom2  20103  dmdprd  20128  dprddisj  20139  dprdf1o  20162  dprdsn  20166  dprd2da  20172  dprd2db  20173  dmdprdsplit2lem  20175  lspuni0  21195  lss0v  21201  zrhval  21721  zrhval2  21722  zrhpropd  21728  isbasisg  23173  basis1  23176  baspartn  23180  tgval  23181  eltg  23183  ntrfval  23250  ntrval  23262  tgrest  23385  restuni2  23393  lmfval  23458  cnfval  23459  cnpfval  23460  pnrmopn  23569  fiuncmp  23630  cmpfi  23634  ptval  23797  ptpjpre1  23798  elptr2  23801  ptuni2  23803  ptbasin  23804  ptbasfi  23808  xkoval  23814  txtopon  23818  ptuni  23821  ptunimpt  23822  xkouni  23826  ptpjcn  23838  ptcld  23840  dfac14  23845  ptcnp  23849  prdstopn  23855  ptrescn  23866  txcmplem2  23869  xkoptsub  23881  xkopt  23882  qtopval  23922  qtopeu  23943  hmphindis  24024  txswaphmeolem  24031  ptuncnv  24034  ptunhmeo  24035  xpstopnlem1  24036  flimval  24190  fcfval  24260  alexsubALTlem3  24276  ptcmplem1  24279  ptcmplem2  24280  ptcmplem3  24281  ptcmplem4  24282  ptcmpg  24284  cnextfres1  24295  cldsubg  24338  utopval  24459  tusval  24492  tuslem  24493  tususs  24496  ucnval  24503  prdsxmslem2  24756  ishtpy  25201  pi1buni  25269  pi1xfrcnv  25286  elovolmr  25705  ovoliunlem3  25733  uniioombllem2  25812  uniioombllem3  25814  dyadmbl  25829  vmaval  27347  vmappw  27350  madeval  28095  oldval  28097  madeoldsuc  28148  unidifsnel  32996  unidifsnne  32997  disjabrex  33042  disjabrexf  33043  fnpreimac  33130  fcnvgreu  33132  xrge0tsmseq  33502  cycpm2tr  33546  lmicqusker  33834  ricqusker  33842  esplyfval1  34070  dimval  34098  dimvalfi  34099  algextdeglem4  34217  algextdeg  34222  locfinreflem  34337  locfinref  34338  pstmval  34392  pstmfval  34393  ordtprsuni  34416  esumeq12dvaf  34528  esumeq2  34533  esumval  34543  esumf1o  34547  esumsnf  34561  esumss  34569  esumpfinval  34572  esumpfinvalf  34573  sigapildsys  34660  sxsigon  34690  meascnbl  34717  brae  34739  braew  34740  faeval  34744  imambfm  34760  cnmbfm  34761  dya2iocuni  34781  omsval  34791  omsfval  34792  omsf  34794  oms0  34795  omssubaddlem  34797  omssubadd  34798  carsgval  34801  carsgclctunlem3  34818  omsmeas  34821  elprob  34907  probfinmeasb  34926  probmeasb  34928  dstrvprob  34970  fineqvnttrclselem1  35634  fineqvnttrclselem2  35635  fineqvnttrclselem3  35636  fineqvnttrclse  35637  fineqvr1ombregs  35651  wevgblacfn  35695  indispconn  35800  iscvm  35825  cvmscld  35839  msrfval  36103  msrval  36104  mthmpps  36148  rdgprc0  36357  rdgprc  36358  dfrdg2  36359  dfrdg3  36360  unisnif  36489  brapply  36502  cbviotadavw  36876  isfne  36945  fnemeet2  36973  fnejoin2  36975  tailfval  36978  ordcmp  37053  ttcid  37098  bj-imafv  37990  mptsnunlem  38079  dissneqlem  38081  ctbssinf  38147  ptrest  38355  mblfinlem2  38394  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  nfunidALT2  39829  nfunidALT  39830  mapdunirnN  42510  zndvdchrrhm  42826  aks6d1c7lem2  43034  aks5lem4a  43043  prjcrvfval  43464  aomclem8  43889  dfac21  43894  rp-unirabeq  44050  rp-tfslim  44181  oaun2  44209  oaun3  44210  ismnu  45072  mnuprdlem1  45083  mnuprdlem2  45084  grumnudlem  45096  grumnud  45097  ismnushort  45112  restuni6  45941  stoweidlem39  46854  salgenuni  47152  caragenval  47308  isome  47309  omeiunle  47332  isomennd  47346  unidmovn  47428  rrnmbl  47429  unidmvon  47432  hspmbl  47444  ovolval4lem2  47465  ovolval5lem2  47468  ovolval5lem3  47469  ovolval5  47470  ovnovollem2  47472  tmachlem-tpopen  47756  tmachlem-uassst  47758  afv2eq12d  48090  uniimaelsetpreimafv  48283  fundcmpsurinjlem3  48287  imasetpreimafvbijlemfo  48292  fundcmpsurbijinjpreimafv  48294  dftpos5  49787  tposideq  49801  restcls2lem  49826  mreclat  49910  toplatglb  49914  swapf1a  50182  swapf2a  50184  swapf1  50185  swapf2  50187  setrecseq  50598