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  4459  relcoi1  5211  resasplitss  5449  fvun1  5639  fmptapd  5765  fvunsng  5768  fnsnsplitss  5773  tfr1onlemaccex  6424  tfrcllemaccex  6437  rdgeq1  6447  rdgivallem  6457  rdgisuc1  6460  rdgon  6462  rdg0  6463  oav2  6539  oasuc  6540  omv2  6541  omsuc  6548  fnsnsplitdc  6581  unsnfidcex  6999  undifdc  7003  fiintim  7010  ssfirab  7015  fnfi  7020  fidcenumlemr  7039  sbthlemi5  7045  sbthlemi6  7046  pm54.43  7280  fzsuc  10173  fseq1p1m1  10198  fseq1m1p1  10199  fzosplitsnm1  10319  fzosplitsn  10343  fzosplitprm1  10344  resunimafz0  10957  zfz1isolemsplit  10964  fsumm1  11646  fprodm1  11828  ennnfonelemp1  12696  ennnfonelemhdmp1  12699  ennnfonelemkh  12702  ennnfonelemhf1o  12703  ennnfonelemnn0  12712  strsetsid  12784  setscom  12791  lspun0  14105  bj-charfundcALT  15609