Theorem difeq12d 4081

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3900

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  csbdif  4480  xpord2pred  8097  xpord3pred  8104  boxcutc  8891  unfilem3  9219  infdifsn  9578  cantnfp1lem3  9601  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  domtriomlem  10364  domtriom  10365  alephsuc3  10503  symgfixelsi  19376  pmtrprfval  19428  dprdf1o  19975  isirred  20367  isdrng  20678  isdrngd  20710  isdrngdOLD  20712  drngpropd  20714  issubdrg  20725  subdrgint  20748  islbs  21040  lbspropd  21063  lssacsex  21111  lspsnat  21112  frlmlbs  21764  islindf  21779  lindfmm  21794  lsslindf  21797  psdmullem  22120  ptcld  23569  iundisj  25517  iundisj2  25518  iunmbl  25522  volsup  25525  dchrval  27213  newval  27843  ltslpss  27916  leslss  27917  nbgrval  29421  nbgr1vtx  29443  iundisjf  32675  iundisj2f  32676  iundisjfi  32886  iundisj2fi  32887  lindfpropd  33474  opprqusdrng  33585  rprmval  33608  isufd  33632  sradrng  33758  qtophaus  34013  zrhunitpreima  34153  meascnbl  34396  brae  34418  braew  34419  ballotlemfrc  34704  reprdifc  34804  chtvalz  34806  onvf1odlem3  35318  satffunlem2lem2  35619  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem9  37877  poimirlem13  37881  poimirlem14  37882  poimirlem16  37884  poimirlem19  37887  voliunnfl  37912  itg2addnclem  37919  isdivrngo  38198  drngoi  38199  lsatset  39363  watfvalN  40365  mapdpglem26  42071  mapdpglem27  42072  hvmapffval  42131  hvmapfval  42132  hvmap1o2  42138  prjspval  42958  prjspnvs  42975  cantnfresb  43678  tfsconcatun  43691  tfsconcat0i  43699  dssmapfvd  44370  fzdifsuc2  45669  stoweidlem34  46389  subsalsal  46714  iundjiunlem  46814  iundjiun  46815  meaiuninc  46836  carageniuncllem1  46876  carageniuncl  46878  hspdifhsp  46971