Theorem unieqd 4884

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 17	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1541  ∪ cuni 4870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871

This theorem is referenced by:  uniprgOLD  4890  unisn3  4894  csbuni  4902  unisn2  5274  opswap  6186  unixpid  6241  iotaeq  6466  iotabi  6467  uniabio  6468  iotanul  6479  funfv  6933  funfv2  6934  fvun  6936  dffv2  6941  fniunfv  7199  ordunisuc  7772  orduniss2  7773  onsucuni2  7774  elxp4  7864  elxp5  7865  1stval  7928  2ndval  7929  1stnpr  7930  2ndnpr  7931  fo1st  7946  fo2nd  7947  f1stres  7950  f2ndres  7951  1st2val  7954  2nd2val  7955  2nd1st  7975  cnvf1olem  8047  brtpos2  8168  dftpos4  8181  tpostpos  8182  frecseq123  8218  csbfrecsg  8220  wrecseq123OLD  8251  tz7.44-2  8358  tz7.44-3  8359  rdglim2  8383  ixpsnf1o  8883  xpcomco  9013  xpassen  9017  xpdom2  9018  supeq1  9390  supeq2  9393  supeq3  9394  supeq123d  9395  supval2  9400  rankuni  9808  en2other2  9954  dfac2a  10074  dfac12lem1  10088  dfac12r  10091  kmlem9  10103  kmlem11  10105  kmlem12  10106  enfin2i  10266  fin23lem29  10286  fin23lem30  10287  fin23lem32  10289  fin23lem34  10291  fin23lem35  10292  fin23lem36  10293  fin23lem38  10294  fin23lem39  10295  fin23lem41  10297  isf34lem7  10324  isf34lem6  10325  fin1a2lem10  10354  fin1a2lem11  10355  fin1a2lem12  10356  itunisuc  10364  itunitc  10366  ttukeylem3  10456  ttukey2g  10461  pwcfsdom  10528  gruurn  10743  dfinfre  12145  relexpfld  14946  relexpfldd  14947  fsumcnv  15669  fprodcnv  15877  mrcun  17516  isacs1i  17551  mreacs  17552  arwval  17943  ipoval  18433  isacs5lem  18448  acsdrscl  18449  acsficl  18450  isps  18471  isdir  18501  pmtrval  19247  pmtrfv  19248  pmtrprfv  19249  pmtrdifellem3  19274  pmtrprfval  19283  gsumcom2  19766  dmdprd  19791  dprddisj  19802  dprdf1o  19825  dprdsn  19829  dprd2da  19835  dprd2db  19836  dmdprdsplit2lem  19838  lspuni0  20528  lss0v  20534  zrhval  20945  zrhval2  20946  zrhpropd  20952  isbasisg  22334  basis1  22337  baspartn  22341  tgval  22342  eltg  22344  ntrfval  22412  ntrval  22424  tgrest  22547  restuni2  22555  lmfval  22620  cnfval  22621  cnpfval  22622  pnrmopn  22731  fiuncmp  22792  cmpfi  22796  ptval  22958  ptpjpre1  22959  elptr2  22962  ptuni2  22964  ptbasin  22965  ptbasfi  22969  xkoval  22975  txtopon  22979  ptuni  22982  ptunimpt  22983  xkouni  22987  ptpjcn  22999  ptcld  23001  dfac14  23006  ptcnp  23010  prdstopn  23016  ptrescn  23027  txcmplem2  23030  xkoptsub  23042  xkopt  23043  qtopval  23083  qtopeu  23104  hmphindis  23185  txswaphmeolem  23192  ptuncnv  23195  ptunhmeo  23196  xpstopnlem1  23197  flimval  23351  fcfval  23421  alexsubALTlem3  23437  ptcmplem1  23440  ptcmplem2  23441  ptcmplem3  23442  ptcmplem4  23443  ptcmpg  23445  cnextfres1  23456  cldsubg  23499  utopval  23621  tusval  23654  tuslem  23655  tuslemOLD  23656  tususs  23659  ucnval  23666  prdsxmslem2  23922  ishtpy  24372  pi1buni  24440  pi1xfrcnv  24457  elovolmr  24877  ovoliunlem3  24905  uniioombllem2  24984  uniioombllem3  24986  dyadmbl  25001  vmaval  26499  vmappw  26502  madeval  27225  oldval  27227  madeoldsuc  27257  unidifsnel  31526  unidifsnne  31527  disjabrex  31567  disjabrexf  31568  fnpreimac  31654  fcnvgreu  31656  xrge0tsmseq  31971  cycpm2tr  32038  qustrivr  32225  ghmquskerlem1  32269  ghmquskerco  32270  dimval  32384  dimvalfi  32385  locfinreflem  32510  locfinref  32511  pstmval  32565  pstmfval  32566  ordtprsuni  32589  esumeq12dvaf  32719  esumeq2  32724  esumval  32734  esumf1o  32738  esumsnf  32752  esumss  32760  esumpfinval  32763  esumpfinvalf  32764  sigapildsys  32850  sxsigon  32880  meascnbl  32907  brae  32929  braew  32930  faeval  32934  imambfm  32951  cnmbfm  32952  dya2iocuni  32972  omsval  32982  omsfval  32983  omsf  32985  oms0  32986  omssubaddlem  32988  omssubadd  32989  carsgval  32992  carsgclctunlem3  33009  omsmeas  33012  elprob  33098  probfinmeasb  33117  probmeasb  33119  dstrvprob  33160  indispconn  33915  iscvm  33940  cvmscld  33954  msrfval  34218  msrval  34219  mthmpps  34263  rdgprc0  34454  rdgprc  34455  dfrdg2  34456  dfrdg3  34457  unisnif  34586  brapply  34599  isfne  34887  fnemeet2  34915  fnejoin2  34917  tailfval  34920  ordcmp  34995  bj-imafv  35795  mptsnunlem  35882  dissneqlem  35884  ctbssinf  35950  ptrest  36150  mblfinlem2  36189  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  nfunidALT2  37504  nfunidALT  37505  mapdunirnN  40186  prjcrvfval  41027  aomclem8  41446  dfac21  41451  rp-unirabeq  41614  rp-tfslim  41746  oaun2  41774  oaun3  41775  ismnu  42663  mnuprdlem1  42674  mnuprdlem2  42675  grumnudlem  42687  grumnud  42688  ismnushort  42703  restuni6  43454  stoweidlem39  44400  salgenuni  44698  caragenval  44854  isome  44855  omeiunle  44878  isomennd  44892  unidmovn  44974  rrnmbl  44975  unidmvon  44978  hspmbl  44990  ovolval4lem2  45011  ovolval5lem2  45014  ovolval5lem3  45015  ovolval5  45016  ovnovollem2  45018  afv2eq12d  45567  uniimaelsetpreimafv  45708  fundcmpsurinjlem3  45712  imasetpreimafvbijlemfo  45717  fundcmpsurbijinjpreimafv  45719  restcls2lem  47065  mreclat  47142  toplatglb  47146  setrecseq  47250