Theorem uneq2d 3303

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

Syntax hints:   → wi 4   = wceq 1363   ∪ cun 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-v 2753  df-un 3147

This theorem is referenced by:  ifeq2  3552  tpeq3  3694  iununir  3984  unisucg  4428  relcoi1  5174  resasplitss  5409  fvun1  5597  fmptapd  5722  fvunsng  5725  fnsnsplitss  5730  tfr1onlemaccex  6366  tfrcllemaccex  6379  rdgeq1  6389  rdgivallem  6399  rdgisuc1  6402  rdgon  6404  rdg0  6405  oav2  6481  oasuc  6482  omv2  6483  omsuc  6490  fnsnsplitdc  6523  unsnfidcex  6936  undifdc  6940  fiintim  6945  ssfirab  6950  fnfi  6953  fidcenumlemr  6971  sbthlemi5  6977  sbthlemi6  6978  pm54.43  7206  fzsuc  10086  fseq1p1m1  10111  fseq1m1p1  10112  fzosplitsnm1  10226  fzosplitsn  10250  fzosplitprm1  10251  resunimafz0  10828  zfz1isolemsplit  10835  fsumm1  11441  fprodm1  11623  ennnfonelemp1  12424  ennnfonelemhdmp1  12427  ennnfonelemkh  12430  ennnfonelemhf1o  12431  ennnfonelemnn0  12440  strsetsid  12512  setscom  12519  lspun0  13701  bj-charfundcALT  14944