Theorem difeq12d 4122

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3944

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-dif 3950

This theorem is referenced by:  csbdif  4526  xpord2pred  8133  xpord3pred  8140  boxcutc  8937  unfilem3  9314  infdifsn  9654  cantnfp1lem3  9677  isf32lem6  10355  isf32lem7  10356  isf32lem8  10357  domtriomlem  10439  domtriom  10440  alephsuc3  10577  symgfixelsi  19344  pmtrprfval  19396  dprdf1o  19943  isirred  20310  isdrng  20504  isdrngd  20533  isdrngdOLD  20535  drngpropd  20537  issubdrg  20544  subdrgint  20562  islbs  20831  lbspropd  20854  lssacsex  20902  lspsnat  20903  frlmlbs  21571  islindf  21586  lindfmm  21601  lsslindf  21604  ptcld  23337  iundisj  25297  iundisj2  25298  iunmbl  25302  volsup  25305  dchrval  26973  newval  27587  sltlpss  27638  slelss  27639  nbgrval  28860  nbgr1vtx  28882  iundisjf  32087  iundisj2f  32088  iundisjfi  32274  iundisj2fi  32275  lindfpropd  32772  opprqusdrng  32881  rprmval  32907  sradrng  32958  qtophaus  33114  zrhunitpreima  33256  meascnbl  33515  brae  33537  braew  33538  ballotlemfrc  33823  reprdifc  33937  chtvalz  33939  satffunlem2lem2  34695  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem9  36800  poimirlem13  36804  poimirlem14  36805  poimirlem16  36807  poimirlem19  36810  voliunnfl  36835  itg2addnclem  36842  isdivrngo  37121  drngoi  37122  lsatset  38163  watfvalN  39166  mapdpglem26  40872  mapdpglem27  40873  hvmapffval  40932  hvmapfval  40933  hvmap1o2  40939  prjspval  41647  prjspnvs  41664  cantnfresb  42376  tfsconcatun  42389  tfsconcat0i  42397  dssmapfvd  43070  fzdifsuc2  44318  stoweidlem34  45048  subsalsal  45373  iundjiunlem  45473  iundjiun  45474  meaiuninc  45495  carageniuncllem1  45535  carageniuncl  45537  hspdifhsp  45630