Theorem unieqd 3832

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

Syntax hints:   → wi 4   = wceq 1363  ∪ cuni 3821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-uni 3822

This theorem is referenced by:  uniprg  3836  unisng  3838  unisn3  4457  onsucuni2  4575  opswapg  5127  elxp4  5128  elxp5  5129  iotaeq  5198  iotabi  5199  uniabio  5200  funfvdm  5592  funfvdm2  5593  fvun1  5595  fniunfv  5776  funiunfvdm  5777  1stvalg  6157  2ndvalg  6158  fo1st  6172  fo2nd  6173  f1stres  6174  f2ndres  6175  2nd1st  6195  cnvf1olem  6239  brtpos2  6266  dftpos4  6278  tpostpos  6279  recseq  6321  tfrexlem  6349  ixpsnf1o  6750  xpcomco  6840  xpassen  6844  xpdom2  6845  supeq1  6999  supeq2  7002  supeq3  7003  supeq123d  7004  en2other2  7209  dfinfre  8927  hashinfom  10772  hashennn  10774  fsumcnv  11459  fprodcnv  11647  tgval  12729  ptex  12731  lssuni  13552  lspuni0  13613  lss0v  13619  isbasisg  13840  basis1  13843  baspartn  13846  eltg  13848  ntrfval  13896  ntrval  13906  tgrest  13965  restuni2  13973  lmfval  13988  cnfval  13990  cnpfval  13991  txtopon  14058  txswaphmeolem  14116  peano4nninf  15052