Theorem uneq1d 3325

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

Syntax hints:   → wi 4   = wceq 1372   ∪ cun 3163

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169

This theorem is referenced by:  ifeq1  3573  preq1  3709  tpeq1  3718  tpeq2  3719  resasplitss  5449  fmptpr  5766  funresdfunsnss  5777  rdgisucinc  6461  oasuc  6540  omsuc  6548  funresdfunsndc  6582  fisseneq  7013  sbthlemi5  7045  exmidfodomrlemim  7291  fzpred  10174  fseq1p1m1  10198  nn0split  10240  nnsplit  10241  fzo0sn0fzo1  10331  fzosplitprm1  10344  zsupcllemstep  10353  fsum1p  11648  fprod1p  11829  setsvala  12782  setsabsd  12790  setscom  12791  prdsex  13019  prdsval  13023  plyaddlem1  15137  plymullem1  15138