Theorem difeq12d 4137

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 4135	. 2 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3		difeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	difeq2d 4136	. 2 ⊢ (𝜑 → (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷))
5	2, 4	eqtrd 2775	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷))

Syntax hints:   → wi 4   = wceq 1537   ∖ cdif 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-dif 3966

This theorem is referenced by:  csbdif  4530  xpord2pred  8169  xpord3pred  8176  boxcutc  8980  unfilem3  9343  infdifsn  9695  cantnfp1lem3  9718  isf32lem6  10396  isf32lem7  10397  isf32lem8  10398  domtriomlem  10480  domtriom  10481  alephsuc3  10618  symgfixelsi  19468  pmtrprfval  19520  dprdf1o  20067  isirred  20436  isdrng  20750  isdrngd  20782  isdrngdOLD  20784  drngpropd  20786  issubdrg  20798  subdrgint  20821  islbs  21093  lbspropd  21116  lssacsex  21164  lspsnat  21165  frlmlbs  21835  islindf  21850  lindfmm  21865  lsslindf  21868  psdmullem  22187  ptcld  23637  iundisj  25597  iundisj2  25598  iunmbl  25602  volsup  25605  dchrval  27293  newval  27909  sltlpss  27960  slelss  27961  nbgrval  29368  nbgr1vtx  29390  iundisjf  32609  iundisj2f  32610  iundisjfi  32804  iundisj2fi  32805  lindfpropd  33390  opprqusdrng  33501  rprmval  33524  isufd  33548  sradrng  33613  qtophaus  33797  zrhunitpreima  33939  meascnbl  34200  brae  34222  braew  34223  ballotlemfrc  34508  reprdifc  34621  chtvalz  34623  satffunlem2lem2  35391  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem9  37616  poimirlem13  37620  poimirlem14  37621  poimirlem16  37623  poimirlem19  37626  voliunnfl  37651  itg2addnclem  37658  isdivrngo  37937  drngoi  37938  lsatset  38972  watfvalN  39975  mapdpglem26  41681  mapdpglem27  41682  hvmapffval  41741  hvmapfval  41742  hvmap1o2  41748  prjspval  42590  prjspnvs  42607  cantnfresb  43314  tfsconcatun  43327  tfsconcat0i  43335  dssmapfvd  44007  fzdifsuc2  45261  stoweidlem34  45990  subsalsal  46315  iundjiunlem  46415  iundjiun  46416  meaiuninc  46437  carageniuncllem1  46477  carageniuncl  46479  hspdifhsp  46572