Theorem uneq2d 3291

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

Syntax hints:   → wi 4   = wceq 1353   ∪ cun 3129

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135

This theorem is referenced by:  ifeq2  3540  tpeq3  3682  iununir  3972  unisucg  4416  relcoi1  5162  resasplitss  5397  fvun1  5584  fmptapd  5709  fvunsng  5712  fnsnsplitss  5717  tfr1onlemaccex  6351  tfrcllemaccex  6364  rdgeq1  6374  rdgivallem  6384  rdgisuc1  6387  rdgon  6389  rdg0  6390  oav2  6466  oasuc  6467  omv2  6468  omsuc  6475  fnsnsplitdc  6508  unsnfidcex  6921  undifdc  6925  fiintim  6930  ssfirab  6935  fnfi  6938  fidcenumlemr  6956  sbthlemi5  6962  sbthlemi6  6963  pm54.43  7191  fzsuc  10071  fseq1p1m1  10096  fseq1m1p1  10097  fzosplitsnm1  10211  fzosplitsn  10235  fzosplitprm1  10236  resunimafz0  10813  zfz1isolemsplit  10820  fsumm1  11426  fprodm1  11608  ennnfonelemp1  12409  ennnfonelemhdmp1  12412  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemnn0  12425  strsetsid  12497  setscom  12504  bj-charfundcALT  14600