Theorem difeq12d 4150

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

Syntax hints:   → wi 4   = wceq 1537   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-dif 3979

This theorem is referenced by:  csbdif  4547  xpord2pred  8186  xpord3pred  8193  boxcutc  8999  unfilem3  9373  infdifsn  9726  cantnfp1lem3  9749  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  domtriomlem  10511  domtriom  10512  alephsuc3  10649  symgfixelsi  19477  pmtrprfval  19529  dprdf1o  20076  isirred  20445  isdrng  20755  isdrngd  20787  isdrngdOLD  20789  drngpropd  20791  issubdrg  20803  subdrgint  20826  islbs  21098  lbspropd  21121  lssacsex  21169  lspsnat  21170  frlmlbs  21840  islindf  21855  lindfmm  21870  lsslindf  21873  psdmullem  22192  ptcld  23642  iundisj  25602  iundisj2  25603  iunmbl  25607  volsup  25610  dchrval  27296  newval  27912  sltlpss  27963  slelss  27964  nbgrval  29371  nbgr1vtx  29393  iundisjf  32611  iundisj2f  32612  iundisjfi  32801  iundisj2fi  32802  lindfpropd  33375  opprqusdrng  33486  rprmval  33509  isufd  33533  sradrng  33598  qtophaus  33782  zrhunitpreima  33924  meascnbl  34183  brae  34205  braew  34206  ballotlemfrc  34491  reprdifc  34604  chtvalz  34606  satffunlem2lem2  35374  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem19  37599  voliunnfl  37624  itg2addnclem  37631  isdivrngo  37910  drngoi  37911  lsatset  38946  watfvalN  39949  mapdpglem26  41655  mapdpglem27  41656  hvmapffval  41715  hvmapfval  41716  hvmap1o2  41722  prjspval  42558  prjspnvs  42575  cantnfresb  43286  tfsconcatun  43299  tfsconcat0i  43307  dssmapfvd  43979  fzdifsuc2  45225  stoweidlem34  45955  subsalsal  46280  iundjiunlem  46380  iundjiun  46381  meaiuninc  46402  carageniuncllem1  46442  carageniuncl  46444  hspdifhsp  46537