Theorem difeq12d 4107

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-dif 3934

This theorem is referenced by:  csbdif  4504  xpord2pred  8149  xpord3pred  8156  boxcutc  8960  unfilem3  9322  infdifsn  9676  cantnfp1lem3  9699  isf32lem6  10377  isf32lem7  10378  isf32lem8  10379  domtriomlem  10461  domtriom  10462  alephsuc3  10599  symgfixelsi  19421  pmtrprfval  19473  dprdf1o  20020  isirred  20384  isdrng  20698  isdrngd  20730  isdrngdOLD  20732  drngpropd  20734  issubdrg  20745  subdrgint  20768  islbs  21039  lbspropd  21062  lssacsex  21110  lspsnat  21111  frlmlbs  21762  islindf  21777  lindfmm  21792  lsslindf  21795  psdmullem  22108  ptcld  23556  iundisj  25506  iundisj2  25507  iunmbl  25511  volsup  25514  dchrval  27202  newval  27820  sltlpss  27876  slelss  27877  nbgrval  29320  nbgr1vtx  29342  iundisjf  32575  iundisj2f  32576  iundisjfi  32778  iundisj2fi  32779  lindfpropd  33402  opprqusdrng  33513  rprmval  33536  isufd  33560  sradrng  33627  qtophaus  33872  zrhunitpreima  34012  meascnbl  34255  brae  34277  braew  34278  ballotlemfrc  34564  reprdifc  34664  chtvalz  34666  satffunlem2lem2  35433  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem9  37658  poimirlem13  37662  poimirlem14  37663  poimirlem16  37665  poimirlem19  37668  voliunnfl  37693  itg2addnclem  37700  isdivrngo  37979  drngoi  37980  lsatset  39013  watfvalN  40016  mapdpglem26  41722  mapdpglem27  41723  hvmapffval  41782  hvmapfval  41783  hvmap1o2  41789  prjspval  42593  prjspnvs  42610  cantnfresb  43315  tfsconcatun  43328  tfsconcat0i  43336  dssmapfvd  44008  fzdifsuc2  45306  stoweidlem34  46030  subsalsal  46355  iundjiunlem  46455  iundjiun  46456  meaiuninc  46477  carageniuncllem1  46517  carageniuncl  46519  hspdifhsp  46612