Theorem unieqd 4850

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

Syntax hints:   → wi 4   = wceq 1539  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  uniprgOLD  4856  unisn3  4859  csbuni  4867  unisn2  5231  opswap  6121  unixpid  6176  iotaeq  6389  iotabi  6390  uniabio  6391  iotanul  6396  funfv  6837  funfv2  6838  fvun  6840  dffv2  6845  fniunfv  7102  ordunisuc  7654  orduniss2  7655  onsucuni2  7656  elxp4  7743  elxp5  7744  1stval  7806  2ndval  7807  1stnpr  7808  2ndnpr  7809  fo1st  7824  fo2nd  7825  f1stres  7828  f2ndres  7829  1st2val  7832  2nd2val  7833  2nd1st  7852  cnvf1olem  7921  brtpos2  8019  dftpos4  8032  tpostpos  8033  frecseq123  8069  csbfrecsg  8071  wrecseq123OLD  8102  tz7.44-2  8209  tz7.44-3  8210  rdglim2  8234  ixpsnf1o  8684  xpcomco  8802  xpassen  8806  xpdom2  8807  supeq1  9134  supeq2  9137  supeq3  9138  supeq123d  9139  supval2  9144  trpredeq1  9398  trpredeq2  9399  trpredeq3  9400  rankuni  9552  en2other2  9696  dfac2a  9816  dfac12lem1  9830  dfac12r  9833  kmlem9  9845  kmlem11  9847  kmlem12  9848  enfin2i  10008  fin23lem29  10028  fin23lem30  10029  fin23lem32  10031  fin23lem34  10033  fin23lem35  10034  fin23lem36  10035  fin23lem38  10036  fin23lem39  10037  fin23lem41  10039  isf34lem7  10066  isf34lem6  10067  fin1a2lem10  10096  fin1a2lem11  10097  fin1a2lem12  10098  itunisuc  10106  itunitc  10108  ttukeylem3  10198  ttukey2g  10203  pwcfsdom  10270  gruurn  10485  dfinfre  11886  relexpfld  14688  relexpfldd  14689  fsumcnv  15413  fprodcnv  15621  mrcun  17248  isacs1i  17283  mreacs  17284  arwval  17674  ipoval  18163  isacs5lem  18178  acsdrscl  18179  acsficl  18180  isps  18201  isdir  18231  pmtrval  18974  pmtrfv  18975  pmtrprfv  18976  pmtrdifellem3  19001  pmtrprfval  19010  gsumcom2  19491  dmdprd  19516  dprddisj  19527  dprdf1o  19550  dprdsn  19554  dprd2da  19560  dprd2db  19561  dmdprdsplit2lem  19563  lspuni0  20187  lss0v  20193  zrhval  20621  zrhval2  20622  zrhpropd  20628  isbasisg  22005  basis1  22008  baspartn  22012  tgval  22013  eltg  22015  ntrfval  22083  ntrval  22095  tgrest  22218  restuni2  22226  lmfval  22291  cnfval  22292  cnpfval  22293  pnrmopn  22402  fiuncmp  22463  cmpfi  22467  ptval  22629  ptpjpre1  22630  elptr2  22633  ptuni2  22635  ptbasin  22636  ptbasfi  22640  xkoval  22646  txtopon  22650  ptuni  22653  ptunimpt  22654  xkouni  22658  ptpjcn  22670  ptcld  22672  dfac14  22677  ptcnp  22681  prdstopn  22687  ptrescn  22698  txcmplem2  22701  xkoptsub  22713  xkopt  22714  qtopval  22754  qtopeu  22775  hmphindis  22856  txswaphmeolem  22863  ptuncnv  22866  ptunhmeo  22867  xpstopnlem1  22868  flimval  23022  fcfval  23092  alexsubALTlem3  23108  ptcmplem1  23111  ptcmplem2  23112  ptcmplem3  23113  ptcmplem4  23114  ptcmpg  23116  cnextfres1  23127  cldsubg  23170  utopval  23292  tusval  23325  tuslem  23326  tuslemOLD  23327  tususs  23330  ucnval  23337  prdsxmslem2  23591  ishtpy  24041  pi1buni  24109  pi1xfrcnv  24126  elovolmr  24545  ovoliunlem3  24573  uniioombllem2  24652  uniioombllem3  24654  dyadmbl  24669  vmaval  26167  vmappw  26170  unidifsnel  30784  unidifsnne  30785  disjabrex  30822  disjabrexf  30823  fnpreimac  30910  fcnvgreu  30912  xrge0tsmseq  31221  cycpm2tr  31288  qustrivr  31463  dimval  31588  dimvalfi  31589  locfinreflem  31692  locfinref  31693  pstmval  31747  pstmfval  31748  ordtprsuni  31771  esumeq12dvaf  31899  esumeq2  31904  esumval  31914  esumf1o  31918  esumsnf  31932  esumss  31940  esumpfinval  31943  esumpfinvalf  31944  sigapildsys  32030  sxsigon  32060  meascnbl  32087  brae  32109  braew  32110  faeval  32114  imambfm  32129  cnmbfm  32130  dya2iocuni  32150  omsval  32160  omsfval  32161  omsf  32163  oms0  32164  omssubaddlem  32166  omssubadd  32167  carsgval  32170  carsgclctunlem3  32187  omsmeas  32190  elprob  32276  probfinmeasb  32295  probmeasb  32297  dstrvprob  32338  indispconn  33096  iscvm  33121  cvmscld  33135  msrfval  33399  msrval  33400  mthmpps  33444  rdgprc0  33675  rdgprc  33676  dfrdg2  33677  dfrdg3  33678  madeval  33963  oldval  33965  madeoldsuc  33994  unisnif  34154  brapply  34167  isfne  34455  fnemeet2  34483  fnejoin2  34485  tailfval  34488  ordcmp  34563  bj-imafv  35349  mptsnunlem  35436  dissneqlem  35438  ctbssinf  35504  ptrest  35703  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  nfunidALT2  36910  nfunidALT  36911  mapdunirnN  39591  aomclem8  40802  dfac21  40807  ismnu  41768  mnuprdlem1  41779  mnuprdlem2  41780  grumnudlem  41792  grumnud  41793  ismnushort  41808  restuni6  42560  stoweidlem39  43470  salgenuni  43766  caragenval  43921  isome  43922  omeiunle  43945  isomennd  43959  unidmovn  44041  rrnmbl  44042  unidmvon  44045  hspmbl  44057  ovolval4lem2  44078  ovolval5lem2  44081  ovolval5lem3  44082  ovolval5  44083  ovnovollem2  44085  afv2eq12d  44594  uniimaelsetpreimafv  44736  fundcmpsurinjlem3  44740  imasetpreimafvbijlemfo  44745  fundcmpsurbijinjpreimafv  44747  restcls2lem  46094  mreclat  46171  toplatglb  46175  setrecseq  46277