Theorem uneq2d 3326

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

Syntax hints:   → wi 4   = wceq 1372   ∪ cun 3163

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169

This theorem is referenced by:  ifeq2  3574  tpeq3  3720  iununir  4010  unisucg  4460  relcoi1  5213  resasplitss  5454  fvun1  5644  fmptapd  5774  fvunsng  5777  fnsnsplitss  5782  tfr1onlemaccex  6433  tfrcllemaccex  6446  rdgeq1  6456  rdgivallem  6466  rdgisuc1  6469  rdgon  6471  rdg0  6472  oav2  6548  oasuc  6549  omv2  6550  omsuc  6557  fnsnsplitdc  6590  unsnfidcex  7016  undifdc  7020  fiintim  7027  ssfirab  7032  fnfi  7037  fidcenumlemr  7056  sbthlemi5  7062  sbthlemi6  7063  pm54.43  7297  fzsuc  10190  fseq1p1m1  10215  fseq1m1p1  10216  fzosplitsnm1  10336  fzosplitsn  10360  fzosplitprm1  10361  resunimafz0  10974  zfz1isolemsplit  10981  fsumm1  11669  fprodm1  11851  ennnfonelemp1  12719  ennnfonelemhdmp1  12722  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemnn0  12735  strsetsid  12807  setscom  12814  lspun0  14129  bj-charfundcALT  15678