Theorem difeq12d 4078

Description: Equality deduction for class difference. (Contributed by FL, 29-May-2014.)

Hypotheses

Ref	Expression
difeq12d.1	⊢ (𝜑 → 𝐴 = 𝐵)
difeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
difeq12d	⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))

Proof of Theorem difeq12d

Step	Hyp	Ref	Expression
1		difeq12d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	difeq1d 4076	. 2 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3		difeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	difeq2d 4077	. 2 ⊢ (𝜑 → (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷))
5	2, 4	eqtrd 2797	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∖ cdif 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-dif 3905

This theorem is used by:  csbdif  4484  xpord2pred  8147  xpord3pred  8154  boxcutc  8952  unfilem3  9281  infdifsn  9640  cantnfp1lem3  9663  isf32lem6  10364  isf32lem7  10365  isf32lem8  10366  domtriomlem  10448  domtriom  10449  alephsuc3  10593  symgfixelsi  19568  pmtrprfval  19620  dprdf1o  20167  isirred  20566  isdrng  20900  isdrngd  20937  isdrngdOLD  20939  drngpropd  20942  issubdrg  20952  subdrgint  20975  islbs  21266  lbspropd  21289  lssacsex  21337  lspsnat  21338  frlmlbs  22016  islindf  22031  lindfmm  22046  lsslindf  22049  psdmullem  22399  ptcld  23845  iundisj  25782  iundisj2  25783  iunmbl  25787  volsup  25790  dchrval  27478  newval  28108  ltslpss  28181  leslss  28182  nbgrval  29804  nbgr1vtx  29826  iundisjf  33070  iundisj2f  33071  iundisjfi  33275  iundisj2fi  33276  lindfpropd  33823  opprqusdrng  33903  rprmval  33934  isufd  33958  sradrng  34100  qtophaus  34354  zrhunitpreima  34494  meascnbl  34738  brae  34760  braew  34761  ballotlemfrc  35046  reprdifc  35143  chtvalz  35145  onvf1odlem3  35710  satffunlem2lem2  35993  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem9  38386  poimirlem13  38390  poimirlem14  38391  poimirlem16  38393  poimirlem19  38396  voliunnfl  38421  itg2addnclem  38428  isdivrngo  38708  drngoi  38709  lsatset  39871  watfvalN  40873  mapdpglem26  42579  mapdpglem27  42580  hvmapffval  42639  hvmapfval  42640  hvmap1o2  42646  prjspval  43457  prjspnvs  43474  cantnfresb  44173  tfsconcatun  44186  tfsconcat0i  44194  dssmapfvd  44865  fzdifsuc2  46151  stoweidlem34  46870  subsalsal  47195  iundjiunlem  47295  iundjiun  47296  meaiuninc  47317  carageniuncllem1  47357  carageniuncl  47359  hspdifhsp  47452