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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∪ cuni 4871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872

This theorem is used by:  unisn3  4892  csbuni  4902  unisn2  5274  opswap  6229  unixpid  6285  iotaeq  6504  iotabi  6505  uniabio  6506  iotanul  6516  funfv  6968  funfv2  6969  fvun  6971  dffv2  6976  fniunfv  7245  ordunisuc  7826  orduniss2  7827  onsucuni2  7828  elxp4  7917  elxp5  7918  1stval  7986  2ndval  7987  1stnpr  7988  2ndnpr  7989  fo1st  8004  fo2nd  8005  f1stres  8008  f2ndres  8009  1st2val  8012  2nd2val  8013  2nd1st  8033  cnvf1olem  8103  brtpos2  8226  dftpos4  8239  tpostpos  8240  frecseq123  8277  csbfrecsg  8279  tz7.44-2  8392  tz7.44-3  8393  rdglim2  8417  ixpsnf1o  8934  xpcomco  9053  xpassen  9057  xpdom2  9058  supeq1  9403  supeq2  9406  supeq3  9407  supeq123d  9408  supval2  9413  rankuni  9833  en2other2  10000  dfac2a  10120  dfac12lem1  10134  dfac12r  10137  kmlem9  10149  kmlem11  10151  kmlem12  10152  enfin2i  10311  fin23lem29  10331  fin23lem30  10332  fin23lem32  10334  fin23lem34  10336  fin23lem35  10337  fin23lem36  10338  fin23lem38  10339  fin23lem39  10340  fin23lem41  10342  isf34lem7  10369  isf34lem6  10370  fin1a2lem10  10399  fin1a2lem11  10400  fin1a2lem12  10401  itunisuc  10409  itunitc  10411  ttukeylem3  10501  ttukey2g  10506  pwcfsdom  10574  gruurn  10789  dfinfre  12202  relexpfld  15093  relexpfldd  15094  fsumcnv  15831  fprodcnv  16044  mrcun  17684  isacs1i  17719  mreacs  17720  arwval  18106  ipoval  18592  isacs5lem  18607  acsdrscl  18608  acsficl  18609  isps  18630  isdir  18660  qustrivr  19259  ghmqusnsglem1  19356  ghmquskerlem1  19359  ghmquskerco  19360  gicqusker  19364  pmtrval  19527  pmtrfv  19528  pmtrprfv  19529  pmtrdifellem3  19554  pmtrprfval  19563  gsumcom2  20051  dmdprd  20076  dprddisj  20087  dprdf1o  20110  dprdsn  20114  dprd2da  20120  dprd2db  20121  dmdprdsplit2lem  20123  lspuni0  21142  lss0v  21148  zrhval  21668  zrhval2  21669  zrhpropd  21675  isbasisg  23115  basis1  23118  baspartn  23122  tgval  23123  eltg  23125  ntrfval  23192  ntrval  23204  tgrest  23327  restuni2  23335  lmfval  23400  cnfval  23401  cnpfval  23402  pnrmopn  23511  fiuncmp  23572  cmpfi  23576  ptval  23738  ptpjpre1  23739  elptr2  23742  ptuni2  23744  ptbasin  23745  ptbasfi  23749  xkoval  23755  txtopon  23759  ptuni  23762  ptunimpt  23763  xkouni  23767  ptpjcn  23779  ptcld  23781  dfac14  23786  ptcnp  23790  prdstopn  23796  ptrescn  23807  txcmplem2  23810  xkoptsub  23822  xkopt  23823  qtopval  23863  qtopeu  23884  hmphindis  23965  txswaphmeolem  23972  ptuncnv  23975  ptunhmeo  23976  xpstopnlem1  23977  flimval  24131  fcfval  24201  alexsubALTlem3  24217  ptcmplem1  24220  ptcmplem2  24221  ptcmplem3  24222  ptcmplem4  24223  ptcmpg  24225  cnextfres1  24236  cldsubg  24279  utopval  24400  tusval  24433  tuslem  24434  tususs  24437  ucnval  24444  prdsxmslem2  24697  ishtpy  25142  pi1buni  25210  pi1xfrcnv  25227  elovolmr  25646  ovoliunlem3  25674  uniioombllem2  25753  uniioombllem3  25755  dyadmbl  25770  vmaval  27288  vmappw  27291  madeval  28036  oldval  28038  madeoldsuc  28089  unidifsnel  32892  unidifsnne  32893  disjabrex  32938  disjabrexf  32939  fnpreimac  33026  fcnvgreu  33028  xrge0tsmseq  33404  cycpm2tr  33448  lmicqusker  33736  ricqusker  33744  esplyfval1  33972  dimval  34000  dimvalfi  34001  algextdeglem4  34119  algextdeg  34124  locfinreflem  34239  locfinref  34240  pstmval  34294  pstmfval  34295  ordtprsuni  34318  esumeq12dvaf  34430  esumeq2  34435  esumval  34445  esumf1o  34449  esumsnf  34463  esumss  34471  esumpfinval  34474  esumpfinvalf  34475  sigapildsys  34561  sxsigon  34591  meascnbl  34618  brae  34640  braew  34641  faeval  34645  imambfm  34661  cnmbfm  34662  dya2iocuni  34682  omsval  34692  omsfval  34693  omsf  34695  oms0  34696  omssubaddlem  34698  omssubadd  34699  carsgval  34702  carsgclctunlem3  34719  omsmeas  34722  elprob  34808  probfinmeasb  34827  probmeasb  34829  dstrvprob  34871  fineqvnttrclselem1  35542  fineqvnttrclselem2  35543  fineqvnttrclselem3  35544  fineqvnttrclse  35545  fineqvr1ombregs  35559  wevgblacfn  35603  indispconn  35734  iscvm  35759  cvmscld  35773  msrfval  36037  msrval  36038  mthmpps  36082  rdgprc0  36291  rdgprc  36292  dfrdg2  36293  dfrdg3  36294  unisnif  36423  brapply  36436  cbviotadavw  36809  isfne  36878  fnemeet2  36906  fnejoin2  36908  tailfval  36911  ordcmp  36986  ttcid  37031  bj-imafv  37923  mptsnunlem  38012  dissneqlem  38014  ctbssinf  38080  ptrest  38298  mblfinlem2  38337  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  nfunidALT2  39771  nfunidALT  39772  mapdunirnN  42452  zndvdchrrhm  42768  aks6d1c7lem2  42976  aks5lem4a  42985  prjcrvfval  43391  aomclem8  43816  dfac21  43821  rp-unirabeq  43977  rp-tfslim  44108  oaun2  44136  oaun3  44137  ismnu  44999  mnuprdlem1  45010  mnuprdlem2  45011  grumnudlem  45023  grumnud  45024  ismnushort  45039  restuni6  45868  stoweidlem39  46781  salgenuni  47079  caragenval  47235  isome  47236  omeiunle  47259  isomennd  47273  unidmovn  47355  rrnmbl  47356  unidmvon  47359  hspmbl  47371  ovolval4lem2  47392  ovolval5lem2  47395  ovolval5lem3  47396  ovolval5  47397  ovnovollem2  47399  afv2eq12d  47980  uniimaelsetpreimafv  48173  fundcmpsurinjlem3  48177  imasetpreimafvbijlemfo  48182  fundcmpsurbijinjpreimafv  48184  dftpos5  49680  tposideq  49694  restcls2lem  49719  mreclat  49803  toplatglb  49807  swapf1a  50075  swapf2a  50077  swapf1  50078  swapf2  50080  setrecseq  50491