Theorem difeq12d 4068

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

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

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 3391  df-dif 3893

This theorem is referenced by:  csbdif  4466  xpord2pred  8088  xpord3pred  8095  boxcutc  8882  unfilem3  9210  infdifsn  9569  cantnfp1lem3  9592  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  domtriomlem  10355  domtriom  10356  alephsuc3  10494  symgfixelsi  19401  pmtrprfval  19453  dprdf1o  20000  isirred  20390  isdrng  20701  isdrngd  20733  isdrngdOLD  20735  drngpropd  20737  issubdrg  20748  subdrgint  20771  islbs  21063  lbspropd  21086  lssacsex  21134  lspsnat  21135  frlmlbs  21787  islindf  21802  lindfmm  21817  lsslindf  21820  psdmullem  22141  ptcld  23588  iundisj  25525  iundisj2  25526  iunmbl  25530  volsup  25533  dchrval  27211  newval  27841  ltslpss  27914  leslss  27915  nbgrval  29419  nbgr1vtx  29441  iundisjf  32674  iundisj2f  32675  iundisjfi  32884  iundisj2fi  32885  lindfpropd  33457  opprqusdrng  33568  rprmval  33591  isufd  33615  sradrng  33741  qtophaus  33996  zrhunitpreima  34136  meascnbl  34379  brae  34401  braew  34402  ballotlemfrc  34687  reprdifc  34787  chtvalz  34789  onvf1odlem3  35303  satffunlem2lem2  35604  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem13  37968  poimirlem14  37969  poimirlem16  37971  poimirlem19  37974  voliunnfl  37999  itg2addnclem  38006  isdivrngo  38285  drngoi  38286  lsatset  39450  watfvalN  40452  mapdpglem26  42158  mapdpglem27  42159  hvmapffval  42218  hvmapfval  42219  hvmap1o2  42225  prjspval  43050  prjspnvs  43067  cantnfresb  43770  tfsconcatun  43783  tfsconcat0i  43791  dssmapfvd  44462  fzdifsuc2  45761  stoweidlem34  46480  subsalsal  46805  iundjiunlem  46905  iundjiun  46906  meaiuninc  46927  carageniuncllem1  46967  carageniuncl  46969  hspdifhsp  47062