Theorem unieqd 4871

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

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

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 3438  df-ss 3920  df-uni 4859

This theorem is referenced by:  unisn3  4879  csbuni  4887  unisn2  5251  opswap  6178  unixpid  6232  iotaeq  6450  iotabi  6451  uniabio  6452  iotanul  6462  funfv  6910  funfv2  6911  fvun  6913  dffv2  6918  fniunfv  7183  ordunisuc  7765  orduniss2  7766  onsucuni2  7767  elxp4  7855  elxp5  7856  1stval  7926  2ndval  7927  1stnpr  7928  2ndnpr  7929  fo1st  7944  fo2nd  7945  f1stres  7948  f2ndres  7949  1st2val  7952  2nd2val  7953  2nd1st  7973  cnvf1olem  8043  brtpos2  8165  dftpos4  8178  tpostpos  8179  frecseq123  8215  csbfrecsg  8217  tz7.44-2  8329  tz7.44-3  8330  rdglim2  8354  ixpsnf1o  8865  xpcomco  8984  xpassen  8988  xpdom2  8989  supeq1  9335  supeq2  9338  supeq3  9339  supeq123d  9340  supval2  9345  rankuni  9759  en2other2  9903  dfac2a  10024  dfac12lem1  10038  dfac12r  10041  kmlem9  10053  kmlem11  10055  kmlem12  10056  enfin2i  10215  fin23lem29  10235  fin23lem30  10236  fin23lem32  10238  fin23lem34  10240  fin23lem35  10241  fin23lem36  10242  fin23lem38  10243  fin23lem39  10244  fin23lem41  10246  isf34lem7  10273  isf34lem6  10274  fin1a2lem10  10303  fin1a2lem11  10304  fin1a2lem12  10305  itunisuc  10313  itunitc  10315  ttukeylem3  10405  ttukey2g  10410  pwcfsdom  10477  gruurn  10692  dfinfre  12106  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  19159  ghmquskerlem1  19162  ghmquskerco  19163  gicqusker  19167  pmtrval  19330  pmtrfv  19331  pmtrprfv  19332  pmtrdifellem3  19357  pmtrprfval  19366  gsumcom2  19854  dmdprd  19879  dprddisj  19890  dprdf1o  19913  dprdsn  19917  dprd2da  19923  dprd2db  19924  dmdprdsplit2lem  19926  lspuni0  20913  lss0v  20920  zrhval  21414  zrhval2  21415  zrhpropd  21421  isbasisg  22832  basis1  22835  baspartn  22839  tgval  22840  eltg  22842  ntrfval  22909  ntrval  22921  tgrest  23044  restuni2  23052  lmfval  23117  cnfval  23118  cnpfval  23119  pnrmopn  23228  fiuncmp  23289  cmpfi  23293  ptval  23455  ptpjpre1  23456  elptr2  23459  ptuni2  23461  ptbasin  23462  ptbasfi  23466  xkoval  23472  txtopon  23476  ptuni  23479  ptunimpt  23480  xkouni  23484  ptpjcn  23496  ptcld  23498  dfac14  23503  ptcnp  23507  prdstopn  23513  ptrescn  23524  txcmplem2  23527  xkoptsub  23539  xkopt  23540  qtopval  23580  qtopeu  23601  hmphindis  23682  txswaphmeolem  23689  ptuncnv  23692  ptunhmeo  23693  xpstopnlem1  23694  flimval  23848  fcfval  23918  alexsubALTlem3  23934  ptcmplem1  23937  ptcmplem2  23938  ptcmplem3  23939  ptcmplem4  23940  ptcmpg  23942  cnextfres1  23953  cldsubg  23996  utopval  24118  tusval  24151  tuslem  24152  tususs  24155  ucnval  24162  prdsxmslem2  24415  ishtpy  24869  pi1buni  24938  pi1xfrcnv  24955  elovolmr  25375  ovoliunlem3  25403  uniioombllem2  25482  uniioombllem3  25484  dyadmbl  25499  vmaval  27021  vmappw  27024  madeval  27764  oldval  27766  madeoldsuc  27801  zs12bday  28365  unidifsnel  32484  unidifsnne  32485  disjabrex  32531  disjabrexf  32532  fnpreimac  32622  fcnvgreu  32624  xrge0tsmseq  33026  cycpm2tr  33070  qustrivr  33311  lmicqusker  33364  ricqusker  33373  dimval  33583  dimvalfi  33584  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  fineqvnttrclselem1  35090  fineqvnttrclselem2  35091  fineqvnttrclselem3  35092  fineqvnttrclse  35093  wevgblacfn  35102  indispconn  35227  iscvm  35252  cvmscld  35266  msrfval  35530  msrval  35531  mthmpps  35575  rdgprc0  35787  rdgprc  35788  dfrdg2  35789  dfrdg3  35790  unisnif  35919  brapply  35932  cbviotadavw  36263  isfne  36333  fnemeet2  36361  fnejoin2  36363  tailfval  36366  ordcmp  36441  bj-imafv  37245  mptsnunlem  37332  dissneqlem  37334  ctbssinf  37400  ptrest  37619  mblfinlem2  37658  ovoliunnfl  37662  voliunnfl  37664  volsupnfl  37665  nfunidALT2  38968  nfunidALT  38969  mapdunirnN  41649  zndvdchrrhm  41965  aks6d1c7lem2  42174  aks5lem4a  42183  prjcrvfval  42624  aomclem8  43054  dfac21  43059  rp-unirabeq  43215  rp-tfslim  43346  oaun2  43374  oaun3  43375  ismnu  44254  mnuprdlem1  44265  mnuprdlem2  44266  grumnudlem  44278  grumnud  44279  ismnushort  44294  restuni6  45120  stoweidlem39  46040  salgenuni  46338  caragenval  46494  isome  46495  omeiunle  46518  isomennd  46532  unidmovn  46614  rrnmbl  46615  unidmvon  46618  hspmbl  46630  ovolval4lem2  46651  ovolval5lem2  46654  ovolval5lem3  46655  ovolval5  46656  ovnovollem2  46658  afv2eq12d  47219  uniimaelsetpreimafv  47400  fundcmpsurinjlem3  47404  imasetpreimafvbijlemfo  47409  fundcmpsurbijinjpreimafv  47411  dftpos5  48878  tposideq  48892  restcls2lem  48917  mreclat  49001  toplatglb  49005  swapf1a  49274  swapf2a  49276  swapf1  49277  swapf2  49279  setrecseq  49690