Theorem uneq2d 3196

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

Syntax hints:   → wi 4   = wceq 1314   ∪ cun 3035

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-un 3041

This theorem is referenced by:  ifeq2  3444  tpeq3  3577  iununir  3862  unisucg  4296  relcoi1  5028  resasplitss  5260  fvun1  5441  fmptapd  5565  fvunsng  5568  fnsnsplitss  5573  tfr1onlemaccex  6199  tfrcllemaccex  6212  rdgeq1  6222  rdgivallem  6232  rdgisuc1  6235  rdgon  6237  rdg0  6238  oav2  6313  oasuc  6314  omv2  6315  omsuc  6322  fnsnsplitdc  6355  unsnfidcex  6761  undifdc  6765  fiintim  6770  ssfirab  6774  fnfi  6777  fidcenumlemr  6795  sbthlemi5  6801  sbthlemi6  6802  pm54.43  6996  fzsuc  9742  fseq1p1m1  9767  fseq1m1p1  9768  fzosplitsnm1  9879  fzosplitsn  9903  fzosplitprm1  9904  resunimafz0  10467  zfz1isolemsplit  10474  fsumm1  11077  ennnfonelemp1  11764  ennnfonelemhdmp1  11767  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemnn0  11780  strsetsid  11835  setscom  11842