Theorem difeq12d 4093

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

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

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920

This theorem is referenced by:  csbdif  4490  xpord2pred  8127  xpord3pred  8134  boxcutc  8917  unfilem3  9263  infdifsn  9617  cantnfp1lem3  9640  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  domtriomlem  10402  domtriom  10403  alephsuc3  10540  symgfixelsi  19372  pmtrprfval  19424  dprdf1o  19971  isirred  20335  isdrng  20649  isdrngd  20681  isdrngdOLD  20683  drngpropd  20685  issubdrg  20696  subdrgint  20719  islbs  20990  lbspropd  21013  lssacsex  21061  lspsnat  21062  frlmlbs  21713  islindf  21728  lindfmm  21743  lsslindf  21746  psdmullem  22059  ptcld  23507  iundisj  25456  iundisj2  25457  iunmbl  25461  volsup  25464  dchrval  27152  newval  27770  sltlpss  27826  slelss  27827  nbgrval  29270  nbgr1vtx  29292  iundisjf  32525  iundisj2f  32526  iundisjfi  32726  iundisj2fi  32727  lindfpropd  33360  opprqusdrng  33471  rprmval  33494  isufd  33518  sradrng  33585  qtophaus  33833  zrhunitpreima  33973  meascnbl  34216  brae  34238  braew  34239  ballotlemfrc  34525  reprdifc  34625  chtvalz  34627  onvf1odlem3  35099  satffunlem2lem2  35400  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem13  37634  poimirlem14  37635  poimirlem16  37637  poimirlem19  37640  voliunnfl  37665  itg2addnclem  37672  isdivrngo  37951  drngoi  37952  lsatset  38990  watfvalN  39993  mapdpglem26  41699  mapdpglem27  41700  hvmapffval  41759  hvmapfval  41760  hvmap1o2  41766  prjspval  42598  prjspnvs  42615  cantnfresb  43320  tfsconcatun  43333  tfsconcat0i  43341  dssmapfvd  44013  fzdifsuc2  45315  stoweidlem34  46039  subsalsal  46364  iundjiunlem  46464  iundjiun  46465  meaiuninc  46486  carageniuncllem1  46526  carageniuncl  46528  hspdifhsp  46621