Theorem difeq12d 4122

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

Syntax hints:   → wi 4   = wceq 1534   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-dif 3950

This theorem is referenced by:  csbdif  4532  xpord2pred  8159  xpord3pred  8166  boxcutc  8970  unfilem3  9346  infdifsn  9700  cantnfp1lem3  9723  isf32lem6  10401  isf32lem7  10402  isf32lem8  10403  domtriomlem  10485  domtriom  10486  alephsuc3  10623  symgfixelsi  19433  pmtrprfval  19485  dprdf1o  20032  isirred  20401  isdrng  20711  isdrngd  20743  isdrngdOLD  20745  drngpropd  20747  issubdrg  20759  subdrgint  20782  islbs  21054  lbspropd  21077  lssacsex  21125  lspsnat  21126  frlmlbs  21795  islindf  21810  lindfmm  21825  lsslindf  21828  psdmullem  22159  ptcld  23608  iundisj  25568  iundisj2  25569  iunmbl  25573  volsup  25576  dchrval  27263  newval  27879  sltlpss  27930  slelss  27931  nbgrval  29272  nbgr1vtx  29294  iundisjf  32509  iundisj2f  32510  iundisjfi  32698  iundisj2fi  32699  lindfpropd  33257  opprqusdrng  33368  rprmval  33391  isufd  33415  sradrng  33480  qtophaus  33651  zrhunitpreima  33793  meascnbl  34052  brae  34074  braew  34075  ballotlemfrc  34360  reprdifc  34473  chtvalz  34475  satffunlem2lem2  35234  poimirlem4  37325  poimirlem6  37327  poimirlem7  37328  poimirlem9  37330  poimirlem13  37334  poimirlem14  37335  poimirlem16  37337  poimirlem19  37340  voliunnfl  37365  itg2addnclem  37372  isdivrngo  37651  drngoi  37652  lsatset  38688  watfvalN  39691  mapdpglem26  41397  mapdpglem27  41398  hvmapffval  41457  hvmapfval  41458  hvmap1o2  41464  prjspval  42257  prjspnvs  42274  cantnfresb  42990  tfsconcatun  43003  tfsconcat0i  43011  dssmapfvd  43684  fzdifsuc2  44925  stoweidlem34  45655  subsalsal  45980  iundjiunlem  46080  iundjiun  46081  meaiuninc  46102  carageniuncllem1  46142  carageniuncl  46144  hspdifhsp  46237