Theorem uneq2d 3358

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

Syntax hints:   → wi 4   = wceq 1395   ∪ cun 3195

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201

This theorem is referenced by:  ifeq2  3606  tpeq3  3754  iununir  4048  unisucg  4504  relcoi1  5259  resasplitss  5504  fvun1  5699  fmptapd  5829  fvunsng  5832  fnsnsplitss  5837  tfr1onlemaccex  6492  tfrcllemaccex  6505  rdgeq1  6515  rdgivallem  6525  rdgisuc1  6528  rdgon  6530  rdg0  6531  oav2  6607  oasuc  6608  omv2  6609  omsuc  6616  fnsnsplitdc  6649  unsnfidcex  7078  undifdc  7082  fiintim  7089  ssfirab  7094  fnfi  7099  fidcenumlemr  7118  sbthlemi5  7124  sbthlemi6  7125  pm54.43  7359  fzsuc  10261  fseq1p1m1  10286  fseq1m1p1  10287  fzosplitsnm1  10410  fzosplitsn  10434  fzosplitprm1  10435  resunimafz0  11048  zfz1isolemsplit  11055  fsumm1  11922  fprodm1  12104  ennnfonelemp1  12972  ennnfonelemhdmp1  12975  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemnn0  12988  strsetsid  13060  setscom  13067  lspun0  14383  bj-charfundcALT  16130