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 1562  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868

This theorem is referenced by:  unisn3  4888  csbuni  4898  unisn2  5264  opswap  6218  unixpid  6273  iotaeq  6491  iotabi  6492  uniabio  6493  iotanul  6503  funfv  6956  funfv2  6957  fvun  6959  dffv2  6964  fniunfv  7233  ordunisuc  7814  orduniss2  7815  onsucuni2  7816  elxp4  7905  elxp5  7906  1stval  7974  2ndval  7975  1stnpr  7976  2ndnpr  7977  fo1st  7992  fo2nd  7993  f1stres  7996  f2ndres  7997  1st2val  8000  2nd2val  8001  2nd1st  8021  cnvf1olem  8091  brtpos2  8214  dftpos4  8227  tpostpos  8228  frecseq123  8265  csbfrecsg  8267  tz7.44-2  8380  tz7.44-3  8381  rdglim2  8405  ixpsnf1o  8922  xpcomco  9041  xpassen  9045  xpdom2  9046  supeq1  9393  supeq2  9396  supeq3  9397  supeq123d  9398  supval2  9403  rankuni  9823  en2other2  9967  dfac2a  10088  dfac12lem1  10102  dfac12r  10105  kmlem9  10117  kmlem11  10119  kmlem12  10120  enfin2i  10280  fin23lem29  10300  fin23lem30  10301  fin23lem32  10303  fin23lem34  10305  fin23lem35  10306  fin23lem36  10307  fin23lem38  10308  fin23lem39  10309  fin23lem41  10311  isf34lem7  10338  isf34lem6  10339  fin1a2lem10  10368  fin1a2lem11  10369  fin1a2lem12  10370  itunisuc  10378  itunitc  10380  ttukeylem3  10470  ttukey2g  10475  pwcfsdom  10543  gruurn  10758  dfinfre  12175  relexpfld  15064  relexpfldd  15065  fsumcnv  15802  fprodcnv  16015  mrcun  17656  isacs1i  17691  mreacs  17692  arwval  18078  ipoval  18564  isacs5lem  18579  acsdrscl  18580  acsficl  18581  isps  18602  isdir  18632  ghmqusnsglem1  19322  ghmquskerlem1  19325  ghmquskerco  19326  gicqusker  19330  pmtrval  19493  pmtrfv  19494  pmtrprfv  19495  pmtrdifellem3  19520  pmtrprfval  19529  gsumcom2  20017  dmdprd  20042  dprddisj  20053  dprdf1o  20076  dprdsn  20080  dprd2da  20086  dprd2db  20087  dmdprdsplit2lem  20089  lspuni0  21079  lss0v  21085  zrhval  21561  zrhval2  21562  zrhpropd  21568  isbasisg  23009  basis1  23012  baspartn  23016  tgval  23017  eltg  23019  ntrfval  23086  ntrval  23098  tgrest  23221  restuni2  23229  lmfval  23294  cnfval  23295  cnpfval  23296  pnrmopn  23405  fiuncmp  23466  cmpfi  23470  ptval  23632  ptpjpre1  23633  elptr2  23636  ptuni2  23638  ptbasin  23639  ptbasfi  23643  xkoval  23649  txtopon  23653  ptuni  23656  ptunimpt  23657  xkouni  23661  ptpjcn  23673  ptcld  23675  dfac14  23680  ptcnp  23684  prdstopn  23690  ptrescn  23701  txcmplem2  23704  xkoptsub  23716  xkopt  23717  qtopval  23757  qtopeu  23778  hmphindis  23859  txswaphmeolem  23866  ptuncnv  23869  ptunhmeo  23870  xpstopnlem1  23871  flimval  24025  fcfval  24095  alexsubALTlem3  24111  ptcmplem1  24114  ptcmplem2  24115  ptcmplem3  24116  ptcmplem4  24117  ptcmpg  24119  cnextfres1  24130  cldsubg  24173  utopval  24294  tusval  24327  tuslem  24328  tususs  24331  ucnval  24338  prdsxmslem2  24591  ishtpy  25036  pi1buni  25104  pi1xfrcnv  25121  elovolmr  25540  ovoliunlem3  25568  uniioombllem2  25647  uniioombllem3  25649  dyadmbl  25664  vmaval  27179  vmappw  27182  madeval  27927  oldval  27929  madeoldsuc  27980  unidifsnel  32736  unidifsnne  32737  disjabrex  32784  disjabrexf  32785  fnpreimac  32874  fcnvgreu  32876  xrge0tsmseq  33257  cycpm2tr  33301  qustrivr  33553  lmicqusker  33606  ricqusker  33615  esplyfval1  33872  dimval  33900  dimvalfi  33901  algextdeglem4  34019  algextdeg  34024  locfinreflem  34139  locfinref  34140  pstmval  34194  pstmfval  34195  ordtprsuni  34218  esumeq12dvaf  34330  esumeq2  34335  esumval  34345  esumf1o  34349  esumsnf  34363  esumss  34371  esumpfinval  34374  esumpfinvalf  34375  sigapildsys  34461  sxsigon  34491  meascnbl  34518  brae  34540  braew  34541  faeval  34545  imambfm  34561  cnmbfm  34562  dya2iocuni  34582  omsval  34592  omsfval  34593  omsf  34595  oms0  34596  omssubaddlem  34598  omssubadd  34599  carsgval  34602  carsgclctunlem3  34619  omsmeas  34622  elprob  34708  probfinmeasb  34727  probmeasb  34729  dstrvprob  34771  fineqvnttrclselem1  35421  fineqvnttrclselem2  35422  fineqvnttrclselem3  35423  fineqvnttrclse  35424  fineqvr1ombregs  35438  wevgblacfn  35458  indispconn  35589  iscvm  35614  cvmscld  35628  msrfval  35892  msrval  35893  mthmpps  35937  rdgprc0  36146  rdgprc  36147  dfrdg2  36148  dfrdg3  36149  unisnif  36278  brapply  36291  cbviotadavw  36634  isfne  36704  fnemeet2  36732  fnejoin2  36734  tailfval  36737  ordcmp  36812  ttcid  36857  bj-imafv  37748  mptsnunlem  37837  dissneqlem  37839  ctbssinf  37905  ptrest  38123  mblfinlem2  38162  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  nfunidALT2  39598  nfunidALT  39599  mapdunirnN  42279  zndvdchrrhm  42595  aks6d1c7lem2  42803  aks5lem4a  42812  prjcrvfval  43218  aomclem8  43643  dfac21  43648  rp-unirabeq  43804  rp-tfslim  43935  oaun2  43963  oaun3  43964  ismnu  44842  mnuprdlem1  44853  mnuprdlem2  44854  grumnudlem  44866  grumnud  44867  ismnushort  44882  restuni6  45705  stoweidlem39  46618  salgenuni  46916  caragenval  47072  isome  47073  omeiunle  47096  isomennd  47110  unidmovn  47192  rrnmbl  47193  unidmvon  47196  hspmbl  47208  ovolval4lem2  47229  ovolval5lem2  47232  ovolval5lem3  47233  ovolval5  47234  ovnovollem2  47236  afv2eq12d  47814  uniimaelsetpreimafv  48007  fundcmpsurinjlem3  48011  imasetpreimafvbijlemfo  48016  fundcmpsurbijinjpreimafv  48018  dftpos5  49500  tposideq  49514  restcls2lem  49539  mreclat  49623  toplatglb  49627  swapf1a  49895  swapf2a  49897  swapf1  49898  swapf2  49900  setrecseq  50311