Theorem difeq12d 4126

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-dif 3953

This theorem is referenced by:  csbdif  4523  xpord2pred  8171  xpord3pred  8178  boxcutc  8982  unfilem3  9346  infdifsn  9698  cantnfp1lem3  9721  isf32lem6  10399  isf32lem7  10400  isf32lem8  10401  domtriomlem  10483  domtriom  10484  alephsuc3  10621  symgfixelsi  19454  pmtrprfval  19506  dprdf1o  20053  isirred  20420  isdrng  20734  isdrngd  20766  isdrngdOLD  20768  drngpropd  20770  issubdrg  20782  subdrgint  20805  islbs  21076  lbspropd  21099  lssacsex  21147  lspsnat  21148  frlmlbs  21818  islindf  21833  lindfmm  21848  lsslindf  21851  psdmullem  22170  ptcld  23622  iundisj  25584  iundisj2  25585  iunmbl  25589  volsup  25592  dchrval  27279  newval  27895  sltlpss  27946  slelss  27947  nbgrval  29354  nbgr1vtx  29376  iundisjf  32603  iundisj2f  32604  iundisjfi  32799  iundisj2fi  32800  lindfpropd  33411  opprqusdrng  33522  rprmval  33545  isufd  33569  sradrng  33634  qtophaus  33836  zrhunitpreima  33978  meascnbl  34221  brae  34243  braew  34244  ballotlemfrc  34530  reprdifc  34643  chtvalz  34645  satffunlem2lem2  35412  poimirlem4  37632  poimirlem6  37634  poimirlem7  37635  poimirlem9  37637  poimirlem13  37641  poimirlem14  37642  poimirlem16  37644  poimirlem19  37647  voliunnfl  37672  itg2addnclem  37679  isdivrngo  37958  drngoi  37959  lsatset  38992  watfvalN  39995  mapdpglem26  41701  mapdpglem27  41702  hvmapffval  41761  hvmapfval  41762  hvmap1o2  41768  prjspval  42618  prjspnvs  42635  cantnfresb  43342  tfsconcatun  43355  tfsconcat0i  43363  dssmapfvd  44035  fzdifsuc2  45327  stoweidlem34  46054  subsalsal  46379  iundjiunlem  46479  iundjiun  46480  meaiuninc  46501  carageniuncllem1  46541  carageniuncl  46543  hspdifhsp  46636