Theorem unieqd 4852

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

Syntax hints:   → wi 4   = wceq 1537  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839

This theorem is referenced by:  uniprg  4856  unisn3  4859  csbuni  4867  unisn2  5216  opswap  6086  unixpid  6135  iotaeq  6326  iotabi  6327  uniabio  6328  iotanul  6333  funfv  6750  funfv2  6751  fvun  6753  dffv2  6756  fniunfv  7006  ordunisuc  7547  orduniss2  7548  onsucuni2  7549  elxp4  7627  elxp5  7628  1stval  7691  2ndval  7692  1stnpr  7693  2ndnpr  7694  fo1st  7709  fo2nd  7710  f1stres  7713  f2ndres  7714  1st2val  7717  2nd2val  7718  2nd1st  7737  cnvf1olem  7805  brtpos2  7898  dftpos4  7911  tpostpos  7912  wrecseq123  7948  tz7.44-2  8043  tz7.44-3  8044  rdglim2  8068  ixpsnf1o  8502  xpcomco  8607  xpassen  8611  xpdom2  8612  supeq1  8909  supeq2  8912  supeq3  8913  supeq123d  8914  supval2  8919  rankuni  9292  en2other2  9435  dfac2a  9555  dfac12lem1  9569  dfac12r  9572  kmlem9  9584  kmlem11  9586  kmlem12  9587  enfin2i  9743  fin23lem29  9763  fin23lem30  9764  fin23lem32  9766  fin23lem34  9768  fin23lem35  9769  fin23lem36  9770  fin23lem38  9771  fin23lem39  9772  fin23lem41  9774  isf34lem7  9801  isf34lem6  9802  fin1a2lem10  9831  fin1a2lem11  9832  fin1a2lem12  9833  itunisuc  9841  itunitc  9843  ttukeylem3  9933  ttukey2g  9938  pwcfsdom  10005  gruurn  10220  dfinfre  11622  relexpfld  14408  fsumcnv  15128  fprodcnv  15337  mrcun  16893  isacs1i  16928  mreacs  16929  arwval  17303  ipoval  17764  isacs5lem  17779  acsdrscl  17780  acsficl  17781  isps  17812  isdir  17842  pmtrval  18579  pmtrfv  18580  pmtrprfv  18581  pmtrdifellem3  18606  pmtrprfval  18615  gsumcom2  19095  dmdprd  19120  dprddisj  19131  dprdf1o  19154  dprdsn  19158  dprd2da  19164  dprd2db  19165  dmdprdsplit2lem  19167  lspuni0  19782  lss0v  19788  zrhval  20655  zrhval2  20656  zrhpropd  20662  isbasisg  21555  basis1  21558  baspartn  21562  tgval  21563  eltg  21565  ntrfval  21632  ntrval  21644  tgrest  21767  restuni2  21775  lmfval  21840  cnfval  21841  cnpfval  21842  pnrmopn  21951  fiuncmp  22012  cmpfi  22016  ptval  22178  ptpjpre1  22179  elptr2  22182  ptuni2  22184  ptbasin  22185  ptbasfi  22189  xkoval  22195  txtopon  22199  ptuni  22202  ptunimpt  22203  xkouni  22207  ptpjcn  22219  ptcld  22221  dfac14  22226  ptcnp  22230  prdstopn  22236  ptrescn  22247  txcmplem2  22250  xkoptsub  22262  xkopt  22263  qtopval  22303  qtopeu  22324  hmphindis  22405  txswaphmeolem  22412  ptuncnv  22415  ptunhmeo  22416  xpstopnlem1  22417  flimval  22571  fcfval  22641  alexsubALTlem3  22657  ptcmplem1  22660  ptcmplem2  22661  ptcmplem3  22662  ptcmplem4  22663  ptcmpg  22665  cnextfres1  22676  cldsubg  22719  utopval  22841  tusval  22875  tuslem  22876  tususs  22879  ucnval  22886  prdsxmslem2  23139  ishtpy  23576  pi1buni  23644  pi1xfrcnv  23661  elovolmr  24077  ovoliunlem3  24105  uniioombllem2  24184  uniioombllem3  24186  dyadmbl  24201  vmaval  25690  vmappw  25693  unidifsnel  30295  unidifsnne  30296  disjabrex  30332  disjabrexf  30333  fnpreimac  30416  fcnvgreu  30418  xrge0tsmseq  30694  cycpm2tr  30761  qustrivr  30930  dimval  31001  dimvalfi  31002  locfinreflem  31104  locfinref  31105  pstmval  31135  pstmfval  31136  ordtprsuni  31162  esumeq12dvaf  31290  esumeq2  31295  esumval  31305  esumf1o  31309  esumsnf  31323  esumss  31331  esumpfinval  31334  esumpfinvalf  31335  sigapildsys  31421  sxsigon  31451  meascnbl  31478  brae  31500  braew  31501  faeval  31505  imambfm  31520  cnmbfm  31521  dya2iocuni  31541  omsval  31551  omsfval  31552  omsf  31554  oms0  31555  omssubaddlem  31557  omssubadd  31558  carsgval  31561  carsgclctunlem3  31578  omsmeas  31581  elprob  31667  probfinmeasb  31686  probmeasb  31688  dstrvprob  31729  indispconn  32481  iscvm  32506  cvmscld  32520  msrfval  32784  msrval  32785  mthmpps  32829  rdgprc0  33038  rdgprc  33039  dfrdg2  33040  dfrdg3  33041  trpredeq1  33059  trpredeq2  33060  trpredeq3  33061  frecseq123  33119  madeval  33289  unisnif  33386  brapply  33399  isfne  33687  fnemeet2  33715  fnejoin2  33717  tailfval  33720  ordcmp  33795  bj-imafv  34536  csbwrecsg  34611  mptsnunlem  34622  dissneqlem  34624  ctbssinf  34690  ptrest  34906  mblfinlem2  34945  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  nfunidALT2  36120  nfunidALT  36121  mapdunirnN  38801  aomclem8  39710  dfac21  39715  ismnu  40646  mnuprdlem1  40657  mnuprdlem2  40658  grumnudlem  40670  grumnud  40671  restuni6  41437  stoweidlem39  42373  salgenuni  42669  caragenval  42824  isome  42825  omeiunle  42848  isomennd  42862  unidmovn  42944  rrnmbl  42945  unidmvon  42948  hspmbl  42960  ovolval4lem2  42981  ovolval5lem2  42984  ovolval5lem3  42985  ovolval5  42986  ovnovollem2  42988  afv2eq12d  43463  uniimaelsetpreimafv  43605  fundcmpsurinjlem3  43609  imasetpreimafvbijlemfo  43614  fundcmpsurbijinjpreimafv  43616  setrecseq  44837