Theorem difeq12d 4079

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

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904

This theorem is referenced by:  csbdif  4478  xpord2pred  8087  xpord3pred  8094  boxcutc  8879  unfilem3  9207  infdifsn  9566  cantnfp1lem3  9589  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  domtriomlem  10352  domtriom  10353  alephsuc3  10491  symgfixelsi  19364  pmtrprfval  19416  dprdf1o  19963  isirred  20355  isdrng  20666  isdrngd  20698  isdrngdOLD  20700  drngpropd  20702  issubdrg  20713  subdrgint  20736  islbs  21028  lbspropd  21051  lssacsex  21099  lspsnat  21100  frlmlbs  21752  islindf  21767  lindfmm  21782  lsslindf  21785  psdmullem  22108  ptcld  23557  iundisj  25505  iundisj2  25506  iunmbl  25510  volsup  25513  dchrval  27201  newval  27831  ltslpss  27904  leslss  27905  nbgrval  29409  nbgr1vtx  29431  iundisjf  32664  iundisj2f  32665  iundisjfi  32876  iundisj2fi  32877  lindfpropd  33463  opprqusdrng  33574  rprmval  33597  isufd  33621  sradrng  33738  qtophaus  33993  zrhunitpreima  34133  meascnbl  34376  brae  34398  braew  34399  ballotlemfrc  34684  reprdifc  34784  chtvalz  34786  onvf1odlem3  35299  satffunlem2lem2  35600  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem19  37840  voliunnfl  37865  itg2addnclem  37872  isdivrngo  38151  drngoi  38152  lsatset  39250  watfvalN  40252  mapdpglem26  41958  mapdpglem27  41959  hvmapffval  42018  hvmapfval  42019  hvmap1o2  42025  prjspval  42846  prjspnvs  42863  cantnfresb  43566  tfsconcatun  43579  tfsconcat0i  43587  dssmapfvd  44258  fzdifsuc2  45558  stoweidlem34  46278  subsalsal  46603  iundjiunlem  46703  iundjiun  46704  meaiuninc  46725  carageniuncllem1  46765  carageniuncl  46767  hspdifhsp  46860