Theorem uneq1d 3312

Description: Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
uneq1d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Proof of Theorem uneq1d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq1 3306	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   = wceq 1364   ∪ cun 3151

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157

This theorem is referenced by:  ifeq1  3560  preq1  3695  tpeq1  3704  tpeq2  3705  resasplitss  5433  fmptpr  5750  funresdfunsnss  5761  rdgisucinc  6438  oasuc  6517  omsuc  6525  funresdfunsndc  6559  fisseneq  6988  sbthlemi5  7020  exmidfodomrlemim  7261  fzpred  10136  fseq1p1m1  10160  nn0split  10202  nnsplit  10203  fzo0sn0fzo1  10288  fzosplitprm1  10301  fsum1p  11561  fprod1p  11742  zsupcllemstep  12082  setsvala  12649  setsabsd  12657  setscom  12658  prdsex  12880  plyaddlem1  14893  plymullem1  14894