Theorem unieqd 4920

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unisn3  4928  csbuni  4936  unisn2  5312  opswap  6249  unixpid  6304  iotaeq  6526  iotabi  6527  uniabio  6528  iotanul  6539  funfv  6996  funfv2  6997  fvun  6999  dffv2  7004  fniunfv  7267  ordunisuc  7852  orduniss2  7853  onsucuni2  7854  elxp4  7944  elxp5  7945  1stval  8016  2ndval  8017  1stnpr  8018  2ndnpr  8019  fo1st  8034  fo2nd  8035  f1stres  8038  f2ndres  8039  1st2val  8042  2nd2val  8043  2nd1st  8063  cnvf1olem  8135  brtpos2  8257  dftpos4  8270  tpostpos  8271  frecseq123  8307  csbfrecsg  8309  wrecseq123OLD  8340  tz7.44-2  8447  tz7.44-3  8448  rdglim2  8472  ixpsnf1o  8978  xpcomco  9102  xpassen  9106  xpdom2  9107  supeq1  9485  supeq2  9488  supeq3  9489  supeq123d  9490  supval2  9495  rankuni  9903  en2other2  10049  dfac2a  10170  dfac12lem1  10184  dfac12r  10187  kmlem9  10199  kmlem11  10201  kmlem12  10202  enfin2i  10361  fin23lem29  10381  fin23lem30  10382  fin23lem32  10384  fin23lem34  10386  fin23lem35  10387  fin23lem36  10388  fin23lem38  10389  fin23lem39  10390  fin23lem41  10392  isf34lem7  10419  isf34lem6  10420  fin1a2lem10  10449  fin1a2lem11  10450  fin1a2lem12  10451  itunisuc  10459  itunitc  10461  ttukeylem3  10551  ttukey2g  10556  pwcfsdom  10623  gruurn  10838  dfinfre  12249  relexpfld  15088  relexpfldd  15089  fsumcnv  15809  fprodcnv  16019  mrcun  17665  isacs1i  17700  mreacs  17701  arwval  18088  ipoval  18575  isacs5lem  18590  acsdrscl  18591  acsficl  18592  isps  18613  isdir  18643  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmquskerco  19302  gicqusker  19306  pmtrval  19469  pmtrfv  19470  pmtrprfv  19471  pmtrdifellem3  19496  pmtrprfval  19505  gsumcom2  19993  dmdprd  20018  dprddisj  20029  dprdf1o  20052  dprdsn  20056  dprd2da  20062  dprd2db  20063  dmdprdsplit2lem  20065  lspuni0  21008  lss0v  21015  zrhval  21518  zrhval2  21519  zrhpropd  21525  isbasisg  22954  basis1  22957  baspartn  22961  tgval  22962  eltg  22964  ntrfval  23032  ntrval  23044  tgrest  23167  restuni2  23175  lmfval  23240  cnfval  23241  cnpfval  23242  pnrmopn  23351  fiuncmp  23412  cmpfi  23416  ptval  23578  ptpjpre1  23579  elptr2  23582  ptuni2  23584  ptbasin  23585  ptbasfi  23589  xkoval  23595  txtopon  23599  ptuni  23602  ptunimpt  23603  xkouni  23607  ptpjcn  23619  ptcld  23621  dfac14  23626  ptcnp  23630  prdstopn  23636  ptrescn  23647  txcmplem2  23650  xkoptsub  23662  xkopt  23663  qtopval  23703  qtopeu  23724  hmphindis  23805  txswaphmeolem  23812  ptuncnv  23815  ptunhmeo  23816  xpstopnlem1  23817  flimval  23971  fcfval  24041  alexsubALTlem3  24057  ptcmplem1  24060  ptcmplem2  24061  ptcmplem3  24062  ptcmplem4  24063  ptcmpg  24065  cnextfres1  24076  cldsubg  24119  utopval  24241  tusval  24274  tuslem  24275  tuslemOLD  24276  tususs  24279  ucnval  24286  prdsxmslem2  24542  ishtpy  25004  pi1buni  25073  pi1xfrcnv  25090  elovolmr  25511  ovoliunlem3  25539  uniioombllem2  25618  uniioombllem3  25620  dyadmbl  25635  vmaval  27156  vmappw  27159  madeval  27891  oldval  27893  madeoldsuc  27923  zs12bday  28424  unidifsnel  32553  unidifsnne  32554  disjabrex  32595  disjabrexf  32596  fnpreimac  32681  fcnvgreu  32683  xrge0tsmseq  33067  cycpm2tr  33139  qustrivr  33393  lmicqusker  33446  ricqusker  33455  dimval  33651  dimvalfi  33652  algextdeglem4  33761  algextdeg  33766  locfinreflem  33839  locfinref  33840  pstmval  33894  pstmfval  33895  ordtprsuni  33918  esumeq12dvaf  34032  esumeq2  34037  esumval  34047  esumf1o  34051  esumsnf  34065  esumss  34073  esumpfinval  34076  esumpfinvalf  34077  sigapildsys  34163  sxsigon  34193  meascnbl  34220  brae  34242  braew  34243  faeval  34247  imambfm  34264  cnmbfm  34265  dya2iocuni  34285  omsval  34295  omsfval  34296  omsf  34298  oms0  34299  omssubaddlem  34301  omssubadd  34302  carsgval  34305  carsgclctunlem3  34322  omsmeas  34325  elprob  34411  probfinmeasb  34430  probmeasb  34432  dstrvprob  34474  wevgblacfn  35114  indispconn  35239  iscvm  35264  cvmscld  35278  msrfval  35542  msrval  35543  mthmpps  35587  rdgprc0  35794  rdgprc  35795  dfrdg2  35796  dfrdg3  35797  unisnif  35926  brapply  35939  cbviotadavw  36270  isfne  36340  fnemeet2  36368  fnejoin2  36370  tailfval  36373  ordcmp  36448  bj-imafv  37252  mptsnunlem  37339  dissneqlem  37341  ctbssinf  37407  ptrest  37626  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  nfunidALT2  38970  nfunidALT  38971  mapdunirnN  41652  zndvdchrrhm  41972  aks6d1c7lem2  42182  aks5lem4a  42191  prjcrvfval  42641  aomclem8  43073  dfac21  43078  rp-unirabeq  43234  rp-tfslim  43366  oaun2  43394  oaun3  43395  ismnu  44280  mnuprdlem1  44291  mnuprdlem2  44292  grumnudlem  44304  grumnud  44305  ismnushort  44320  restuni6  45127  stoweidlem39  46054  salgenuni  46352  caragenval  46508  isome  46509  omeiunle  46532  isomennd  46546  unidmovn  46628  rrnmbl  46629  unidmvon  46632  hspmbl  46644  ovolval4lem2  46665  ovolval5lem2  46668  ovolval5lem3  46669  ovolval5  46670  ovnovollem2  46672  afv2eq12d  47227  uniimaelsetpreimafv  47383  fundcmpsurinjlem3  47387  imasetpreimafvbijlemfo  47392  fundcmpsurbijinjpreimafv  47394  dftpos5  48774  tposideq  48788  restcls2lem  48810  mreclat  48886  toplatglb  48890  swapf1a  48975  swapf2a  48977  swapf1  48978  swapf2  48980  setrecseq  49204