Theorem difeq12d 4085

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-dif 3911

This theorem is used by:  csbdif  4491  xpord2pred  8150  xpord3pred  8157  boxcutc  8948  unfilem3  9277  infdifsn  9636  cantnfp1lem3  9659  isf32lem6  10360  isf32lem7  10361  isf32lem8  10362  domtriomlem  10444  domtriom  10445  alephsuc3  10583  symgfixelsi  19536  pmtrprfval  19588  dprdf1o  20135  isirred  20534  isdrng  20868  isdrngd  20905  isdrngdOLD  20907  drngpropd  20910  issubdrg  20920  subdrgint  20943  islbs  21234  lbspropd  21257  lssacsex  21305  lspsnat  21306  frlmlbs  21984  islindf  21999  lindfmm  22014  lsslindf  22017  psdmullem  22365  ptcld  23807  iundisj  25744  iundisj2  25745  iunmbl  25749  volsup  25752  dchrval  27435  newval  28065  ltslpss  28138  leslss  28139  nbgrval  29723  nbgr1vtx  29745  iundisjf  32971  iundisj2f  32972  iundisjfi  33178  iundisj2fi  33179  lindfpropd  33726  opprqusdrng  33806  rprmval  33837  isufd  33861  sradrng  34003  qtophaus  34257  zrhunitpreima  34397  meascnbl  34641  brae  34663  braew  34664  ballotlemfrc  34949  reprdifc  35046  chtvalz  35048  onvf1odlem3  35613  satffunlem2lem2  35919  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem9  38321  poimirlem13  38325  poimirlem14  38326  poimirlem16  38328  poimirlem19  38331  voliunnfl  38356  itg2addnclem  38363  isdivrngo  38642  drngoi  38643  lsatset  39805  watfvalN  40807  mapdpglem26  42513  mapdpglem27  42514  hvmapffval  42573  hvmapfval  42574  hvmap1o2  42580  prjspval  43376  prjspnvs  43393  cantnfresb  44092  tfsconcatun  44105  tfsconcat0i  44113  dssmapfvd  44784  fzdifsuc2  46070  stoweidlem34  46789  subsalsal  47114  iundjiunlem  47214  iundjiun  47215  meaiuninc  47236  carageniuncllem1  47276  carageniuncl  47278  hspdifhsp  47371