Theorem difeq12d 4051

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

Syntax hints:   → wi 4   = wceq 1538   ∖ cdif 3878

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-dif 3884

This theorem is referenced by:  boxcutc  8488  unfilem3  8768  infdifsn  9104  cantnfp1lem3  9127  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  domtriomlem  9853  domtriom  9854  alephsuc3  9991  symgfixelsi  18555  pmtrprfval  18607  dprdf1o  19147  isirred  19445  isdrng  19499  isdrngd  19520  drngpropd  19522  issubdrg  19553  subdrgint  19575  islbs  19841  lbspropd  19864  lssacsex  19909  lspsnat  19910  frlmlbs  20486  islindf  20501  lindfmm  20516  lsslindf  20519  ptcld  22218  iundisj  24152  iundisj2  24153  iunmbl  24157  volsup  24160  dchrval  25818  nbgrval  27126  nbgr1vtx  27148  iundisjf  30352  iundisj2f  30353  iundisjfi  30545  iundisj2fi  30546  lindfpropd  30996  rprmval  31072  sradrng  31076  qtophaus  31189  zrhunitpreima  31329  meascnbl  31588  brae  31610  braew  31611  ballotlemfrc  31894  reprdifc  32008  chtvalz  32010  satffunlem2lem2  32766  csbdif  34742  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem9  35066  poimirlem13  35070  poimirlem14  35071  poimirlem16  35073  poimirlem19  35076  voliunnfl  35101  itg2addnclem  35108  isdivrngo  35388  drngoi  35389  lsatset  36286  watfvalN  37288  mapdpglem26  38994  mapdpglem27  38995  hvmapffval  39054  hvmapfval  39055  hvmap1o2  39061  prjspval  39597  dssmapfvd  40718  fzdifsuc2  41942  stoweidlem34  42676  subsalsal  42999  iundjiunlem  43098  iundjiun  43099  meaiuninc  43120  carageniuncllem1  43160  carageniuncl  43162  hspdifhsp  43255