Theorem difeq12d 4076

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

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-dif 3901

This theorem is referenced by:  csbdif  4475  xpord2pred  8083  xpord3pred  8090  boxcutc  8873  unfilem3  9200  infdifsn  9556  cantnfp1lem3  9579  isf32lem6  10258  isf32lem7  10259  isf32lem8  10260  domtriomlem  10342  domtriom  10343  alephsuc3  10480  symgfixelsi  19351  pmtrprfval  19403  dprdf1o  19950  isirred  20341  isdrng  20652  isdrngd  20684  isdrngdOLD  20686  drngpropd  20688  issubdrg  20699  subdrgint  20722  islbs  21014  lbspropd  21037  lssacsex  21085  lspsnat  21086  frlmlbs  21738  islindf  21753  lindfmm  21768  lsslindf  21771  psdmullem  22083  ptcld  23531  iundisj  25479  iundisj2  25480  iunmbl  25484  volsup  25487  dchrval  27175  newval  27799  sltlpss  27856  slelss  27857  nbgrval  29318  nbgr1vtx  29340  iundisjf  32573  iundisj2f  32574  iundisjfi  32785  iundisj2fi  32786  lindfpropd  33356  opprqusdrng  33467  rprmval  33490  isufd  33514  sradrng  33617  qtophaus  33872  zrhunitpreima  34012  meascnbl  34255  brae  34277  braew  34278  ballotlemfrc  34563  reprdifc  34663  chtvalz  34665  onvf1odlem3  35172  satffunlem2lem2  35473  poimirlem4  37687  poimirlem6  37689  poimirlem7  37690  poimirlem9  37692  poimirlem13  37696  poimirlem14  37697  poimirlem16  37699  poimirlem19  37702  voliunnfl  37727  itg2addnclem  37734  isdivrngo  38013  drngoi  38014  lsatset  39112  watfvalN  40114  mapdpglem26  41820  mapdpglem27  41821  hvmapffval  41880  hvmapfval  41881  hvmap1o2  41887  prjspval  42724  prjspnvs  42741  cantnfresb  43444  tfsconcatun  43457  tfsconcat0i  43465  dssmapfvd  44137  fzdifsuc2  45438  stoweidlem34  46159  subsalsal  46484  iundjiunlem  46584  iundjiun  46585  meaiuninc  46606  carageniuncllem1  46646  carageniuncl  46648  hspdifhsp  46741