Theorem difeq12d 4080

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-dif 3908

This theorem is referenced by:  csbdif  4477  xpord2pred  8085  xpord3pred  8092  boxcutc  8875  unfilem3  9214  infdifsn  9572  cantnfp1lem3  9595  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  domtriomlem  10355  domtriom  10356  alephsuc3  10493  symgfixelsi  19332  pmtrprfval  19384  dprdf1o  19931  isirred  20322  isdrng  20636  isdrngd  20668  isdrngdOLD  20670  drngpropd  20672  issubdrg  20683  subdrgint  20706  islbs  20998  lbspropd  21021  lssacsex  21069  lspsnat  21070  frlmlbs  21722  islindf  21737  lindfmm  21752  lsslindf  21755  psdmullem  22068  ptcld  23516  iundisj  25465  iundisj2  25466  iunmbl  25470  volsup  25473  dchrval  27161  newval  27783  sltlpss  27840  slelss  27841  nbgrval  29299  nbgr1vtx  29321  iundisjf  32551  iundisj2f  32552  iundisjfi  32752  iundisj2fi  32753  lindfpropd  33332  opprqusdrng  33443  rprmval  33466  isufd  33490  sradrng  33557  qtophaus  33805  zrhunitpreima  33945  meascnbl  34188  brae  34210  braew  34211  ballotlemfrc  34497  reprdifc  34597  chtvalz  34599  onvf1odlem3  35080  satffunlem2lem2  35381  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem9  37611  poimirlem13  37615  poimirlem14  37616  poimirlem16  37618  poimirlem19  37621  voliunnfl  37646  itg2addnclem  37653  isdivrngo  37932  drngoi  37933  lsatset  38971  watfvalN  39974  mapdpglem26  41680  mapdpglem27  41681  hvmapffval  41740  hvmapfval  41741  hvmap1o2  41747  prjspval  42579  prjspnvs  42596  cantnfresb  43300  tfsconcatun  43313  tfsconcat0i  43321  dssmapfvd  43993  fzdifsuc2  45295  stoweidlem34  46019  subsalsal  46344  iundjiunlem  46444  iundjiun  46445  meaiuninc  46466  carageniuncllem1  46506  carageniuncl  46508  hspdifhsp  46601