Theorem unieqd 3946

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ∪ cuni 3935

This proof depends on 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 proof 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 3936

This theorem is used by:  uniprg  3950  unisng  3952  unisn3  4591  onsucuni2  4711  opswapg  5274  elxp4  5275  elxp5  5276  iotaeq  5346  iotabi  5347  uniabio  5348  funfvdm  5766  funfvdm2  5767  fvun1  5769  fniunfv  5968  funiunfvdm  5969  1stvalg  6376  2ndvalg  6377  fo1st  6391  fo2nd  6392  f1stres  6393  f2ndres  6394  2nd1st  6414  cnvf1olem  6460  brtpos2  6522  dftpos4  6534  tpostpos  6535  recseq  6577  tfrexlem  6605  ixpsnf1o  7018  xpcomco  7124  xpassen  7128  xpdom2  7129  supeq1  7327  supeq2  7330  supeq3  7331  supeq123d  7332  en2other2  7549  dfinfre  9289  hashinfom  11233  hashennn  11235  fsumcnv  12223  fprodcnv  12411  tgval  13669  ptex  13671  lssuni  14784  lspuni0  14845  lss0v  14851  zrhval  15036  zrhvalg  15037  zrhval2  15038  zrhpropd  15045  isbasisg  15236  basis1  15239  baspartn  15242  eltg  15244  ntrfval  15292  ntrval  15302  tgrest  15361  restuni2  15369  lmfval  15385  cnfval  15386  cnpfval  15387  txtopon  15454  txswaphmeolem  15512  peano4nninf  17215