Theorem unieqd 3941

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

Syntax hints:   → wi 4   = wceq 1402  ∪ cuni 3930

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3931

This theorem is referenced by:  uniprg  3945  unisng  3947  unisn3  4586  onsucuni2  4706  opswapg  5269  elxp4  5270  elxp5  5271  iotaeq  5341  iotabi  5342  uniabio  5343  funfvdm  5760  funfvdm2  5761  fvun1  5763  fniunfv  5958  funiunfvdm  5959  1stvalg  6366  2ndvalg  6367  fo1st  6381  fo2nd  6382  f1stres  6383  f2ndres  6384  2nd1st  6404  cnvf1olem  6450  brtpos2  6512  dftpos4  6524  tpostpos  6525  recseq  6567  tfrexlem  6595  ixpsnf1o  7008  xpcomco  7114  xpassen  7118  xpdom2  7119  supeq1  7316  supeq2  7319  supeq3  7320  supeq123d  7321  en2other2  7538  dfinfre  9276  hashinfom  11195  hashennn  11197  fsumcnv  12182  fprodcnv  12370  tgval  13593  ptex  13595  lssuni  14672  lspuni0  14733  lss0v  14739  zrhval  14924  zrhvalg  14925  zrhval2  14926  zrhpropd  14933  isbasisg  15068  basis1  15071  baspartn  15074  eltg  15076  ntrfval  15124  ntrval  15134  tgrest  15193  restuni2  15201  lmfval  15217  cnfval  15218  cnpfval  15219  txtopon  15286  txswaphmeolem  15344  peano4nninf  16954