Theorem unieqd 3686

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

Syntax hints:   → wi 4   = wceq 1296  ∪ cuni 3675

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-uni 3676

This theorem is referenced by:  uniprg  3690  unisng  3692  unisn3  4295  onsucuni2  4408  opswapg  4951  elxp4  4952  elxp5  4953  iotaeq  5022  iotabi  5023  uniabio  5024  funfvdm  5402  funfvdm2  5403  fvun1  5405  fniunfv  5579  funiunfvdm  5580  1stvalg  5951  2ndvalg  5952  fo1st  5966  fo2nd  5967  f1stres  5968  f2ndres  5969  2nd1st  5988  cnvf1olem  6027  brtpos2  6054  dftpos4  6066  tpostpos  6067  recseq  6109  tfrexlem  6137  ixpsnf1o  6533  xpcomco  6622  xpassen  6626  xpdom2  6627  supeq1  6761  supeq2  6764  supeq3  6765  supeq123d  6766  en2other2  6919  dfinfre  8514  hashinfom  10317  hashennn  10319  fsumcnv  10995  isbasisg  11909  basis1  11912  baspartn  11915  tgval  11916  eltg  11919  ntrfval  11967  ntrval  11977  tgrest  12036  restuni2  12044  lmfval  12059  cnfval  12061  cnpfval  12062  peano4nninf  12605