Theorem uneq2d 3271

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

Syntax hints:   → wi 4   = wceq 1342   ∪ cun 3109

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115

This theorem is referenced by:  ifeq2  3519  tpeq3  3658  iununir  3943  unisucg  4386  relcoi1  5129  resasplitss  5361  fvun1  5546  fmptapd  5670  fvunsng  5673  fnsnsplitss  5678  tfr1onlemaccex  6307  tfrcllemaccex  6320  rdgeq1  6330  rdgivallem  6340  rdgisuc1  6343  rdgon  6345  rdg0  6346  oav2  6422  oasuc  6423  omv2  6424  omsuc  6431  fnsnsplitdc  6464  unsnfidcex  6876  undifdc  6880  fiintim  6885  ssfirab  6890  fnfi  6893  fidcenumlemr  6911  sbthlemi5  6917  sbthlemi6  6918  pm54.43  7137  fzsuc  9994  fseq1p1m1  10019  fseq1m1p1  10020  fzosplitsnm1  10134  fzosplitsn  10158  fzosplitprm1  10159  resunimafz0  10730  zfz1isolemsplit  10737  fsumm1  11343  fprodm1  11525  ennnfonelemp1  12276  ennnfonelemhdmp1  12279  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemnn0  12292  strsetsid  12364  setscom  12371  bj-charfundcALT  13526