Theorem difeq12d 4064

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4047

This theorem is used by:  csbdif  4480  xpord2pred  8164  xpord3pred  8171  boxcutc  8972  unfilem3  9302  infdifsn  9661  cantnfp1lem3  9684  isf32lem6  10439  isf32lem7  10440  isf32lem8  10441  domtriomlem  10523  domtriom  10524  alephsuc3  10668  symgfixelsi  19654  pmtrprfval  19706  dprdf1o  20253  isirred  20654  isdrng  20989  isdrngd  21027  isdrngdOLD  21029  drngpropd  21032  issubdrg  21042  subdrgint  21065  islbs  21356  lbspropd  21379  lssacsex  21427  lspsnat  21428  frlmlbs  22108  islindf  22123  lindfmm  22138  lsslindf  22141  psdmullem  22491  ptcld  23937  iundisj  25874  iundisj2  25875  iunmbl  25879  volsup  25882  dchrval  27566  newval  28226  ltslpss  28299  leslss  28300  nbgrval  29922  nbgr1vtx  29944  iundisjf  33230  iundisj2f  33231  iundisjfi  33434  iundisj2fi  33435  lindfpropd  33983  opprqusdrng  34063  rprmval  34094  isufd  34118  sradrng  34260  qtophaus  34514  zrhunitpreima  34654  meascnbl  34898  brae  34920  braew  34921  ballotlemfrc  35205  reprdifc  35302  chtvalz  35304  onvf1odlem3  35952  satffunlem2lem2  36257  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem9  38640  poimirlem13  38644  poimirlem14  38645  poimirlem16  38647  poimirlem19  38650  voliunnfl  38675  itg2addnclem  38682  isdivrngo  38977  drngoi  38978  lsatset  40140  watfvalN  41142  mapdpglem26  42848  mapdpglem27  42849  hvmapffval  42908  hvmapfval  42909  hvmap1o2  42915  prjspval  43724  prjspnvs  43741  cantnfresb  44419  tfsconcatun  44432  tfsconcat0i  44440  dssmapfvd  45110  fzdifsuc2  46419  stoweidlem34  47137  subsalsal  47462  iundjiunlem  47562  iundjiun  47563  meaiuninc  47584  carageniuncllem1  47624  carageniuncl  47626  hspdifhsp  47719