Theorem uneq2d 3361

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

Syntax hints:   → wi 4   = wceq 1397   ∪ cun 3198

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204

This theorem is referenced by:  ifeq2  3609  tpeq3  3759  iununir  4054  unisucg  4511  relcoi1  5268  resasplitss  5516  fvun1  5712  fmptapd  5844  fvunsng  5847  fnsnsplitss  5852  tfr1onlemaccex  6513  tfrcllemaccex  6526  rdgeq1  6536  rdgivallem  6546  rdgisuc1  6549  rdgon  6551  rdg0  6552  oav2  6630  oasuc  6631  omv2  6632  omsuc  6639  fnsnsplitdc  6672  unsnfidcex  7111  undifdc  7115  fiintim  7122  ssfirab  7128  fnfi  7134  fidcenumlemr  7153  sbthlemi5  7159  sbthlemi6  7160  pm54.43  7394  fzsuc  10303  fseq1p1m1  10328  fseq1m1p1  10329  fzosplitsnm1  10453  fzosplitsn  10477  fzosplitpr  10478  fzosplitprm1  10479  resunimafz0  11094  zfz1isolemsplit  11101  fsumm1  11976  fprodm1  12158  ennnfonelemp1  13026  ennnfonelemhdmp1  13029  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemnn0  13042  strsetsid  13114  setscom  13121  lspun0  14438  p1evtxdeqfilem  16161  clwwlknonex2lem1  16287  bj-charfundcALT  16404