Theorem difeq12d 4123

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

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

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-dif 3951

This theorem is referenced by:  csbdif  4527  xpord2pred  8134  xpord3pred  8141  boxcutc  8938  unfilem3  9315  infdifsn  9655  cantnfp1lem3  9678  isf32lem6  10356  isf32lem7  10357  isf32lem8  10358  domtriomlem  10440  domtriom  10441  alephsuc3  10578  symgfixelsi  19345  pmtrprfval  19397  dprdf1o  19944  isirred  20311  isdrng  20505  isdrngd  20534  isdrngdOLD  20536  drngpropd  20538  issubdrg  20545  subdrgint  20563  islbs  20832  lbspropd  20855  lssacsex  20903  lspsnat  20904  frlmlbs  21572  islindf  21587  lindfmm  21602  lsslindf  21605  ptcld  23338  iundisj  25298  iundisj2  25299  iunmbl  25303  volsup  25306  dchrval  26974  newval  27588  sltlpss  27639  slelss  27640  nbgrval  28861  nbgr1vtx  28883  iundisjf  32088  iundisj2f  32089  iundisjfi  32275  iundisj2fi  32276  lindfpropd  32773  opprqusdrng  32882  rprmval  32908  sradrng  32959  qtophaus  33115  zrhunitpreima  33257  meascnbl  33516  brae  33538  braew  33539  ballotlemfrc  33824  reprdifc  33938  chtvalz  33940  satffunlem2lem2  34696  poimirlem4  36796  poimirlem6  36798  poimirlem7  36799  poimirlem9  36801  poimirlem13  36805  poimirlem14  36806  poimirlem16  36808  poimirlem19  36811  voliunnfl  36836  itg2addnclem  36843  isdivrngo  37122  drngoi  37123  lsatset  38164  watfvalN  39167  mapdpglem26  40873  mapdpglem27  40874  hvmapffval  40933  hvmapfval  40934  hvmap1o2  40940  prjspval  41648  prjspnvs  41665  cantnfresb  42377  tfsconcatun  42390  tfsconcat0i  42398  dssmapfvd  43071  fzdifsuc2  44319  stoweidlem34  45049  subsalsal  45374  iundjiunlem  45474  iundjiun  45475  meaiuninc  45496  carageniuncllem1  45536  carageniuncl  45538  hspdifhsp  45631