Theorem uneq2d 3383

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

Syntax hints:   → wi 4   = wceq 1402   ∪ cun 3218

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224

This theorem is referenced by:  ifeq2  3641  tpeq3  3795  iununir  4091  unisucg  4554  relcoi1  5314  resasplitss  5564  fvun1  5763  fmptapd  5897  fvunsng  5900  fnsnsplitss  5905  tfr1onlemaccex  6609  tfrcllemaccex  6622  rdgeq1  6632  rdgivallem  6642  rdgisuc1  6645  rdgon  6647  rdg0  6648  oav2  6726  oasuc  6727  omv2  6728  omsuc  6735  fnsnsplitdc  6768  unsnfidcex  7217  undifdc  7221  fiintim  7228  ssfirab  7234  fnfi  7240  fidcenumlemr  7262  sbthlemi5  7268  sbthlemi6  7269  pm54.43  7526  fzsuc  10453  fzspl  10454  fseq1p1m1  10479  fseq1m1p1  10480  fzosplitsnm1  10605  fzosplitsn  10629  fzosplitpr  10630  fzosplitprm1  10631  resunimafz0  11252  zfz1isolemsplit  11268  fsumm1  12161  fprodm1  12343  ballotfilemfp1  13209  ennnfonelemp1  13275  ennnfonelemhdmp1  13278  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemnn0  13291  strsetsid  13363  setscom  13370  gsump1  14134  lspun0  14734  p1evtxdeqfilem  16466  clwwlknonex2lem1  16592  bj-charfundcALT  16749