Theorem unieqd 3904

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

Syntax hints:   → wi 4   = wceq 1397  ∪ cuni 3893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894

This theorem is referenced by:  uniprg  3908  unisng  3910  unisn3  4542  onsucuni2  4662  opswapg  5223  elxp4  5224  elxp5  5225  iotaeq  5295  iotabi  5296  uniabio  5297  funfvdm  5709  funfvdm2  5710  fvun1  5712  fniunfv  5902  funiunfvdm  5903  1stvalg  6304  2ndvalg  6305  fo1st  6319  fo2nd  6320  f1stres  6321  f2ndres  6322  2nd1st  6342  cnvf1olem  6388  brtpos2  6416  dftpos4  6428  tpostpos  6429  recseq  6471  tfrexlem  6499  ixpsnf1o  6904  xpcomco  7009  xpassen  7013  xpdom2  7014  supeq1  7184  supeq2  7187  supeq3  7188  supeq123d  7189  en2other2  7406  dfinfre  9135  hashinfom  11039  hashennn  11041  fsumcnv  11997  fprodcnv  12185  tgval  13344  ptex  13346  lssuni  14376  lspuni0  14437  lss0v  14443  zrhval  14630  zrhvalg  14631  zrhval2  14632  zrhpropd  14639  isbasisg  14767  basis1  14770  baspartn  14773  eltg  14775  ntrfval  14823  ntrval  14833  tgrest  14892  restuni2  14900  lmfval  14916  cnfval  14917  cnpfval  14918  txtopon  14985  txswaphmeolem  15043  peano4nninf  16608