Theorem unieqd 4901

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889

This theorem is referenced by:  unisn3  4909  csbuni  4917  unisn2  5287  opswap  6223  unixpid  6278  iotaeq  6501  iotabi  6502  uniabio  6503  iotanul  6514  funfv  6971  funfv2  6972  fvun  6974  dffv2  6979  fniunfv  7244  ordunisuc  7831  orduniss2  7832  onsucuni2  7833  elxp4  7923  elxp5  7924  1stval  7995  2ndval  7996  1stnpr  7997  2ndnpr  7998  fo1st  8013  fo2nd  8014  f1stres  8017  f2ndres  8018  1st2val  8021  2nd2val  8022  2nd1st  8042  cnvf1olem  8114  brtpos2  8236  dftpos4  8249  tpostpos  8250  frecseq123  8286  csbfrecsg  8288  wrecseq123OLD  8319  tz7.44-2  8426  tz7.44-3  8427  rdglim2  8451  ixpsnf1o  8957  xpcomco  9081  xpassen  9085  xpdom2  9086  supeq1  9462  supeq2  9465  supeq3  9466  supeq123d  9467  supval2  9472  rankuni  9882  en2other2  10028  dfac2a  10149  dfac12lem1  10163  dfac12r  10166  kmlem9  10178  kmlem11  10180  kmlem12  10181  enfin2i  10340  fin23lem29  10360  fin23lem30  10361  fin23lem32  10363  fin23lem34  10365  fin23lem35  10366  fin23lem36  10367  fin23lem38  10368  fin23lem39  10369  fin23lem41  10371  isf34lem7  10398  isf34lem6  10399  fin1a2lem10  10428  fin1a2lem11  10429  fin1a2lem12  10430  itunisuc  10438  itunitc  10440  ttukeylem3  10530  ttukey2g  10535  pwcfsdom  10602  gruurn  10817  dfinfre  12228  relexpfld  15073  relexpfldd  15074  fsumcnv  15794  fprodcnv  16004  mrcun  17639  isacs1i  17674  mreacs  17675  arwval  18061  ipoval  18545  isacs5lem  18560  acsdrscl  18561  acsficl  18562  isps  18583  isdir  18613  ghmqusnsglem1  19268  ghmquskerlem1  19271  ghmquskerco  19272  gicqusker  19276  pmtrval  19437  pmtrfv  19438  pmtrprfv  19439  pmtrdifellem3  19464  pmtrprfval  19473  gsumcom2  19961  dmdprd  19986  dprddisj  19997  dprdf1o  20020  dprdsn  20024  dprd2da  20030  dprd2db  20031  dmdprdsplit2lem  20033  lspuni0  20972  lss0v  20979  zrhval  21473  zrhval2  21474  zrhpropd  21480  isbasisg  22890  basis1  22893  baspartn  22897  tgval  22898  eltg  22900  ntrfval  22967  ntrval  22979  tgrest  23102  restuni2  23110  lmfval  23175  cnfval  23176  cnpfval  23177  pnrmopn  23286  fiuncmp  23347  cmpfi  23351  ptval  23513  ptpjpre1  23514  elptr2  23517  ptuni2  23519  ptbasin  23520  ptbasfi  23524  xkoval  23530  txtopon  23534  ptuni  23537  ptunimpt  23538  xkouni  23542  ptpjcn  23554  ptcld  23556  dfac14  23561  ptcnp  23565  prdstopn  23571  ptrescn  23582  txcmplem2  23585  xkoptsub  23597  xkopt  23598  qtopval  23638  qtopeu  23659  hmphindis  23740  txswaphmeolem  23747  ptuncnv  23750  ptunhmeo  23751  xpstopnlem1  23752  flimval  23906  fcfval  23976  alexsubALTlem3  23992  ptcmplem1  23995  ptcmplem2  23996  ptcmplem3  23997  ptcmplem4  23998  ptcmpg  24000  cnextfres1  24011  cldsubg  24054  utopval  24176  tusval  24209  tuslem  24210  tususs  24213  ucnval  24220  prdsxmslem2  24473  ishtpy  24927  pi1buni  24996  pi1xfrcnv  25013  elovolmr  25434  ovoliunlem3  25462  uniioombllem2  25541  uniioombllem3  25543  dyadmbl  25558  vmaval  27080  vmappw  27083  madeval  27817  oldval  27819  madeoldsuc  27853  zs12bday  28400  unidifsnel  32521  unidifsnne  32522  disjabrex  32568  disjabrexf  32569  fnpreimac  32654  fcnvgreu  32656  xrge0tsmseq  33063  cycpm2tr  33135  qustrivr  33385  lmicqusker  33438  ricqusker  33447  dimval  33645  dimvalfi  33646  algextdeglem4  33759  algextdeg  33764  locfinreflem  33876  locfinref  33877  pstmval  33931  pstmfval  33932  ordtprsuni  33955  esumeq12dvaf  34067  esumeq2  34072  esumval  34082  esumf1o  34086  esumsnf  34100  esumss  34108  esumpfinval  34111  esumpfinvalf  34112  sigapildsys  34198  sxsigon  34228  meascnbl  34255  brae  34277  braew  34278  faeval  34282  imambfm  34299  cnmbfm  34300  dya2iocuni  34320  omsval  34330  omsfval  34331  omsf  34333  oms0  34334  omssubaddlem  34336  omssubadd  34337  carsgval  34340  carsgclctunlem3  34357  omsmeas  34360  elprob  34446  probfinmeasb  34465  probmeasb  34467  dstrvprob  34509  wevgblacfn  35136  indispconn  35261  iscvm  35286  cvmscld  35300  msrfval  35564  msrval  35565  mthmpps  35609  rdgprc0  35816  rdgprc  35817  dfrdg2  35818  dfrdg3  35819  unisnif  35948  brapply  35961  cbviotadavw  36292  isfne  36362  fnemeet2  36390  fnejoin2  36392  tailfval  36395  ordcmp  36470  bj-imafv  37274  mptsnunlem  37361  dissneqlem  37363  ctbssinf  37429  ptrest  37648  mblfinlem2  37687  ovoliunnfl  37691  voliunnfl  37693  volsupnfl  37694  nfunidALT2  38992  nfunidALT  38993  mapdunirnN  41674  zndvdchrrhm  41990  aks6d1c7lem2  42199  aks5lem4a  42208  prjcrvfval  42629  aomclem8  43060  dfac21  43065  rp-unirabeq  43221  rp-tfslim  43352  oaun2  43380  oaun3  43381  ismnu  44260  mnuprdlem1  44271  mnuprdlem2  44272  grumnudlem  44284  grumnud  44285  ismnushort  44300  restuni6  45126  stoweidlem39  46048  salgenuni  46346  caragenval  46502  isome  46503  omeiunle  46526  isomennd  46540  unidmovn  46622  rrnmbl  46623  unidmvon  46626  hspmbl  46638  ovolval4lem2  46659  ovolval5lem2  46662  ovolval5lem3  46663  ovolval5  46664  ovnovollem2  46666  afv2eq12d  47224  uniimaelsetpreimafv  47390  fundcmpsurinjlem3  47394  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  dftpos5  48829  tposideq  48843  restcls2lem  48867  mreclat  48951  toplatglb  48955  swapf1a  49166  swapf2a  49168  swapf1  49169  swapf2  49171  setrecseq  49529