Theorem unieqd 3822

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

Syntax hints:   → wi 4   = wceq 1353  ∪ cuni 3811

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3812

This theorem is referenced by:  uniprg  3826  unisng  3828  unisn3  4447  onsucuni2  4565  opswapg  5117  elxp4  5118  elxp5  5119  iotaeq  5188  iotabi  5189  uniabio  5190  funfvdm  5581  funfvdm2  5582  fvun1  5584  fniunfv  5765  funiunfvdm  5766  1stvalg  6145  2ndvalg  6146  fo1st  6160  fo2nd  6161  f1stres  6162  f2ndres  6163  2nd1st  6183  cnvf1olem  6227  brtpos2  6254  dftpos4  6266  tpostpos  6267  recseq  6309  tfrexlem  6337  ixpsnf1o  6738  xpcomco  6828  xpassen  6832  xpdom2  6833  supeq1  6987  supeq2  6990  supeq3  6991  supeq123d  6992  en2other2  7197  dfinfre  8915  hashinfom  10760  hashennn  10762  fsumcnv  11447  fprodcnv  11635  tgval  12716  ptex  12718  lssuni  13455  isbasisg  13583  basis1  13586  baspartn  13589  eltg  13591  ntrfval  13639  ntrval  13649  tgrest  13708  restuni2  13716  lmfval  13731  cnfval  13733  cnpfval  13734  txtopon  13801  txswaphmeolem  13859  peano4nninf  14794