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  3529  tpeq3  3669  iununir  3954  unisucg  4397  relcoi1  5140  resasplitss  5375  fvun1  5560  fmptapd  5684  fvunsng  5687  fnsnsplitss  5692  tfr1onlemaccex  6324  tfrcllemaccex  6337  rdgeq1  6347  rdgivallem  6357  rdgisuc1  6360  rdgon  6362  rdg0  6363  oav2  6439  oasuc  6440  omv2  6441  omsuc  6448  fnsnsplitdc  6481  unsnfidcex  6893  undifdc  6897  fiintim  6902  ssfirab  6907  fnfi  6910  fidcenumlemr  6928  sbthlemi5  6934  sbthlemi6  6935  pm54.43  7154  fzsuc  10012  fseq1p1m1  10037  fseq1m1p1  10038  fzosplitsnm1  10152  fzosplitsn  10176  fzosplitprm1  10177  resunimafz0  10753  zfz1isolemsplit  10760  fsumm1  11366  fprodm1  11548  ennnfonelemp1  12348  ennnfonelemhdmp1  12351  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemnn0  12364  strsetsid  12436  setscom  12443  bj-charfundcALT  13766