Theorem difeq12d 4081

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

Syntax hints:   → wi 4   = wceq 1559   ∖ cdif 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3907

This theorem is referenced by:  csbdif  4478  xpord2pred  8120  xpord3pred  8127  boxcutc  8919  unfilem3  9247  infdifsn  9609  cantnfp1lem3  9632  isf32lem6  10312  isf32lem7  10313  isf32lem8  10314  domtriomlem  10396  domtriom  10397  alephsuc3  10535  symgfixelsi  19458  pmtrprfval  19510  dprdf1o  20057  isirred  20447  isdrng  20762  isdrngd  20794  isdrngdOLD  20796  drngpropd  20798  issubdrg  20809  subdrgint  20832  islbs  21123  lbspropd  21146  lssacsex  21194  lspsnat  21195  frlmlbs  21829  islindf  21844  lindfmm  21859  lsslindf  21862  psdmullem  22210  ptcld  23653  iundisj  25590  iundisj2  25591  iunmbl  25595  volsup  25598  dchrval  27275  newval  27905  ltslpss  27978  leslss  27979  nbgrval  29483  nbgr1vtx  29505  iundisjf  32738  iundisj2f  32739  iundisjfi  32948  iundisj2fi  32949  lindfpropd  33529  opprqusdrng  33642  rprmval  33673  isufd  33697  sradrng  33840  qtophaus  34094  zrhunitpreima  34234  meascnbl  34477  brae  34499  braew  34500  ballotlemfrc  34785  reprdifc  34885  chtvalz  34887  onvf1odlem3  35412  satffunlem2lem2  35720  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem9  38092  poimirlem13  38096  poimirlem14  38097  poimirlem16  38099  poimirlem19  38102  voliunnfl  38127  itg2addnclem  38134  isdivrngo  38413  drngoi  38414  lsatset  39578  watfvalN  40580  mapdpglem26  42286  mapdpglem27  42287  hvmapffval  42346  hvmapfval  42347  hvmap1o2  42353  prjspval  43149  prjspnvs  43166  cantnfresb  43865  tfsconcatun  43878  tfsconcat0i  43886  dssmapfvd  44557  fzdifsuc2  45853  stoweidlem34  46572  subsalsal  46897  iundjiunlem  46997  iundjiun  46998  meaiuninc  47019  carageniuncllem1  47059  carageniuncl  47061  hspdifhsp  47154