Theorem difeq12d 4067

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  csbdif  4465  xpord2pred  8095  xpord3pred  8102  boxcutc  8889  unfilem3  9217  infdifsn  9578  cantnfp1lem3  9601  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  domtriomlem  10364  domtriom  10365  alephsuc3  10503  symgfixelsi  19410  pmtrprfval  19462  dprdf1o  20009  isirred  20399  isdrng  20710  isdrngd  20742  isdrngdOLD  20744  drngpropd  20746  issubdrg  20757  subdrgint  20780  islbs  21071  lbspropd  21094  lssacsex  21142  lspsnat  21143  frlmlbs  21777  islindf  21792  lindfmm  21807  lsslindf  21810  psdmullem  22131  ptcld  23578  iundisj  25515  iundisj2  25516  iunmbl  25520  volsup  25523  dchrval  27197  newval  27827  ltslpss  27900  leslss  27901  nbgrval  29405  nbgr1vtx  29427  iundisjf  32659  iundisj2f  32660  iundisjfi  32869  iundisj2fi  32870  lindfpropd  33442  opprqusdrng  33553  rprmval  33576  isufd  33600  sradrng  33726  qtophaus  33980  zrhunitpreima  34120  meascnbl  34363  brae  34385  braew  34386  ballotlemfrc  34671  reprdifc  34771  chtvalz  34773  onvf1odlem3  35287  satffunlem2lem2  35588  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem19  37960  voliunnfl  37985  itg2addnclem  37992  isdivrngo  38271  drngoi  38272  lsatset  39436  watfvalN  40438  mapdpglem26  42144  mapdpglem27  42145  hvmapffval  42204  hvmapfval  42205  hvmap1o2  42211  prjspval  43036  prjspnvs  43053  cantnfresb  43752  tfsconcatun  43765  tfsconcat0i  43773  dssmapfvd  44444  fzdifsuc2  45743  stoweidlem34  46462  subsalsal  46787  iundjiunlem  46887  iundjiun  46888  meaiuninc  46909  carageniuncllem1  46949  carageniuncl  46951  hspdifhsp  47044