Theorem uneq2d 3281

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

Hypothesis

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

Assertion

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

Proof of Theorem uneq2d

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

Syntax hints:   → wi 4   = wceq 1348   ∪ cun 3119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125

This theorem is referenced by:  ifeq2  3530  tpeq3  3671  iununir  3956  unisucg  4399  relcoi1  5142  resasplitss  5377  fvun1  5562  fmptapd  5687  fvunsng  5690  fnsnsplitss  5695  tfr1onlemaccex  6327  tfrcllemaccex  6340  rdgeq1  6350  rdgivallem  6360  rdgisuc1  6363  rdgon  6365  rdg0  6366  oav2  6442  oasuc  6443  omv2  6444  omsuc  6451  fnsnsplitdc  6484  unsnfidcex  6897  undifdc  6901  fiintim  6906  ssfirab  6911  fnfi  6914  fidcenumlemr  6932  sbthlemi5  6938  sbthlemi6  6939  pm54.43  7167  fzsuc  10025  fseq1p1m1  10050  fseq1m1p1  10051  fzosplitsnm1  10165  fzosplitsn  10189  fzosplitprm1  10190  resunimafz0  10766  zfz1isolemsplit  10773  fsumm1  11379  fprodm1  11561  ennnfonelemp1  12361  ennnfonelemhdmp1  12364  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemnn0  12377  strsetsid  12449  setscom  12456  bj-charfundcALT  13844