Theorem unieqd 3899

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

Syntax hints:   → wi 4   = wceq 1395  ∪ cuni 3888

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889

This theorem is referenced by:  uniprg  3903  unisng  3905  unisn3  4536  onsucuni2  4656  opswapg  5215  elxp4  5216  elxp5  5217  iotaeq  5287  iotabi  5288  uniabio  5289  funfvdm  5697  funfvdm2  5698  fvun1  5700  fniunfv  5886  funiunfvdm  5887  1stvalg  6288  2ndvalg  6289  fo1st  6303  fo2nd  6304  f1stres  6305  f2ndres  6306  2nd1st  6326  cnvf1olem  6370  brtpos2  6397  dftpos4  6409  tpostpos  6410  recseq  6452  tfrexlem  6480  ixpsnf1o  6883  xpcomco  6985  xpassen  6989  xpdom2  6990  supeq1  7153  supeq2  7156  supeq3  7157  supeq123d  7158  en2other2  7374  dfinfre  9103  hashinfom  11000  hashennn  11002  fsumcnv  11948  fprodcnv  12136  tgval  13295  ptex  13297  lssuni  14327  lspuni0  14388  lss0v  14394  zrhval  14581  zrhvalg  14582  zrhval2  14583  zrhpropd  14590  isbasisg  14718  basis1  14721  baspartn  14724  eltg  14726  ntrfval  14774  ntrval  14784  tgrest  14843  restuni2  14851  lmfval  14867  cnfval  14868  cnpfval  14869  txtopon  14936  txswaphmeolem  14994  peano4nninf  16372