Theorem unieqd 4864

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

Syntax hints:   → wi 4   = wceq 1542  ∪ cuni 4851

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unisn3  4872  csbuni  4881  unisn2  5248  opswap  6189  unixpid  6244  iotaeq  6462  iotabi  6463  uniabio  6464  iotanul  6474  funfv  6923  funfv2  6924  fvun  6926  dffv2  6931  fniunfv  7197  ordunisuc  7778  orduniss2  7779  onsucuni2  7780  elxp4  7868  elxp5  7869  1stval  7939  2ndval  7940  1stnpr  7941  2ndnpr  7942  fo1st  7957  fo2nd  7958  f1stres  7961  f2ndres  7962  1st2val  7965  2nd2val  7966  2nd1st  7986  cnvf1olem  8055  brtpos2  8177  dftpos4  8190  tpostpos  8191  frecseq123  8227  csbfrecsg  8229  tz7.44-2  8341  tz7.44-3  8342  rdglim2  8366  ixpsnf1o  8881  xpcomco  9000  xpassen  9004  xpdom2  9005  supeq1  9353  supeq2  9356  supeq3  9357  supeq123d  9358  supval2  9363  rankuni  9782  en2other2  9926  dfac2a  10047  dfac12lem1  10061  dfac12r  10064  kmlem9  10076  kmlem11  10078  kmlem12  10079  enfin2i  10238  fin23lem29  10258  fin23lem30  10259  fin23lem32  10261  fin23lem34  10263  fin23lem35  10264  fin23lem36  10265  fin23lem38  10266  fin23lem39  10267  fin23lem41  10269  isf34lem7  10296  isf34lem6  10297  fin1a2lem10  10326  fin1a2lem11  10327  fin1a2lem12  10328  itunisuc  10336  itunitc  10338  ttukeylem3  10428  ttukey2g  10433  pwcfsdom  10501  gruurn  10716  dfinfre  12132  relexpfld  15006  relexpfldd  15007  fsumcnv  15730  fprodcnv  15943  mrcun  17583  isacs1i  17618  mreacs  17619  arwval  18005  ipoval  18491  isacs5lem  18506  acsdrscl  18507  acsficl  18508  isps  18529  isdir  18559  ghmqusnsglem1  19250  ghmquskerlem1  19253  ghmquskerco  19254  gicqusker  19258  pmtrval  19421  pmtrfv  19422  pmtrprfv  19423  pmtrdifellem3  19448  pmtrprfval  19457  gsumcom2  19945  dmdprd  19970  dprddisj  19981  dprdf1o  20004  dprdsn  20008  dprd2da  20014  dprd2db  20015  dmdprdsplit2lem  20017  lspuni0  21000  lss0v  21007  zrhval  21501  zrhval2  21502  zrhpropd  21508  isbasisg  22926  basis1  22929  baspartn  22933  tgval  22934  eltg  22936  ntrfval  23003  ntrval  23015  tgrest  23138  restuni2  23146  lmfval  23211  cnfval  23212  cnpfval  23213  pnrmopn  23322  fiuncmp  23383  cmpfi  23387  ptval  23549  ptpjpre1  23550  elptr2  23553  ptuni2  23555  ptbasin  23556  ptbasfi  23560  xkoval  23566  txtopon  23570  ptuni  23573  ptunimpt  23574  xkouni  23578  ptpjcn  23590  ptcld  23592  dfac14  23597  ptcnp  23601  prdstopn  23607  ptrescn  23618  txcmplem2  23621  xkoptsub  23633  xkopt  23634  qtopval  23674  qtopeu  23695  hmphindis  23776  txswaphmeolem  23783  ptuncnv  23786  ptunhmeo  23787  xpstopnlem1  23788  flimval  23942  fcfval  24012  alexsubALTlem3  24028  ptcmplem1  24031  ptcmplem2  24032  ptcmplem3  24033  ptcmplem4  24034  ptcmpg  24036  cnextfres1  24047  cldsubg  24090  utopval  24211  tusval  24244  tuslem  24245  tususs  24248  ucnval  24255  prdsxmslem2  24508  ishtpy  24953  pi1buni  25021  pi1xfrcnv  25038  elovolmr  25457  ovoliunlem3  25485  uniioombllem2  25564  uniioombllem3  25566  dyadmbl  25581  vmaval  27094  vmappw  27097  madeval  27842  oldval  27844  madeoldsuc  27895  unidifsnel  32624  unidifsnne  32625  disjabrex  32671  disjabrexf  32672  fnpreimac  32762  fcnvgreu  32764  xrge0tsmseq  33155  cycpm2tr  33199  qustrivr  33444  lmicqusker  33497  ricqusker  33506  esplyfval1  33736  dimval  33764  dimvalfi  33765  algextdeglem4  33884  algextdeg  33889  locfinreflem  34004  locfinref  34005  pstmval  34059  pstmfval  34060  ordtprsuni  34083  esumeq12dvaf  34195  esumeq2  34200  esumval  34210  esumf1o  34214  esumsnf  34228  esumss  34236  esumpfinval  34239  esumpfinvalf  34240  sigapildsys  34326  sxsigon  34356  meascnbl  34383  brae  34405  braew  34406  faeval  34410  imambfm  34426  cnmbfm  34427  dya2iocuni  34447  omsval  34457  omsfval  34458  omsf  34460  oms0  34461  omssubaddlem  34463  omssubadd  34464  carsgval  34467  carsgclctunlem3  34484  omsmeas  34487  elprob  34573  probfinmeasb  34592  probmeasb  34594  dstrvprob  34636  fineqvnttrclselem1  35285  fineqvnttrclselem2  35286  fineqvnttrclselem3  35287  fineqvnttrclse  35288  fineqvr1ombregs  35302  wevgblacfn  35311  indispconn  35436  iscvm  35461  cvmscld  35475  msrfval  35739  msrval  35740  mthmpps  35784  rdgprc0  35993  rdgprc  35994  dfrdg2  35995  dfrdg3  35996  unisnif  36125  brapply  36138  cbviotadavw  36471  isfne  36541  fnemeet2  36569  fnejoin2  36571  tailfval  36574  ordcmp  36649  ttcid  36694  bj-imafv  37585  mptsnunlem  37674  dissneqlem  37676  ctbssinf  37742  ptrest  37960  mblfinlem2  37999  ovoliunnfl  38003  voliunnfl  38005  volsupnfl  38006  nfunidALT2  39435  nfunidALT  39436  mapdunirnN  42116  zndvdchrrhm  42432  aks6d1c7lem2  42640  aks5lem4a  42649  prjcrvfval  43084  aomclem8  43513  dfac21  43518  rp-unirabeq  43674  rp-tfslim  43805  oaun2  43833  oaun3  43834  ismnu  44712  mnuprdlem1  44723  mnuprdlem2  44724  grumnudlem  44736  grumnud  44737  ismnushort  44752  restuni6  45576  stoweidlem39  46491  salgenuni  46789  caragenval  46945  isome  46946  omeiunle  46969  isomennd  46983  unidmovn  47065  rrnmbl  47066  unidmvon  47069  hspmbl  47081  ovolval4lem2  47102  ovolval5lem2  47105  ovolval5lem3  47106  ovolval5  47107  ovnovollem2  47109  afv2eq12d  47681  uniimaelsetpreimafv  47874  fundcmpsurinjlem3  47878  imasetpreimafvbijlemfo  47883  fundcmpsurbijinjpreimafv  47885  dftpos5  49367  tposideq  49381  restcls2lem  49406  mreclat  49490  toplatglb  49494  swapf1a  49762  swapf2a  49764  swapf1  49765  swapf2  49767  setrecseq  50178