Theorem difeq12d 4075

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  csbdif  4481  xpord2pred  8146  xpord3pred  8153  boxcutc  8953  unfilem3  9283  infdifsn  9642  cantnfp1lem3  9665  isf32lem6  10417  isf32lem7  10418  isf32lem8  10419  domtriomlem  10501  domtriom  10502  alephsuc3  10646  symgfixelsi  19629  pmtrprfval  19681  dprdf1o  20228  isirred  20629  isdrng  20964  isdrngd  21002  isdrngdOLD  21004  drngpropd  21007  issubdrg  21017  subdrgint  21040  islbs  21331  lbspropd  21354  lssacsex  21402  lspsnat  21403  frlmlbs  22083  islindf  22098  lindfmm  22113  lsslindf  22116  psdmullem  22466  ptcld  23912  iundisj  25849  iundisj2  25850  iunmbl  25854  volsup  25857  dchrval  27543  newval  28203  ltslpss  28276  leslss  28277  nbgrval  29899  nbgr1vtx  29921  iundisjf  33165  iundisj2f  33166  iundisjfi  33370  iundisj2fi  33371  lindfpropd  33919  opprqusdrng  33999  rprmval  34030  isufd  34054  sradrng  34196  qtophaus  34450  zrhunitpreima  34590  meascnbl  34834  brae  34856  braew  34857  ballotlemfrc  35142  reprdifc  35239  chtvalz  35241  onvf1odlem3  35857  satffunlem2lem2  36140  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem9  38515  poimirlem13  38519  poimirlem14  38520  poimirlem16  38522  poimirlem19  38525  voliunnfl  38550  itg2addnclem  38557  isdivrngo  38852  drngoi  38853  lsatset  40015  watfvalN  41017  mapdpglem26  42723  mapdpglem27  42724  hvmapffval  42783  hvmapfval  42784  hvmap1o2  42790  prjspval  43593  prjspnvs  43610  cantnfresb  44284  tfsconcatun  44297  tfsconcat0i  44305  dssmapfvd  44976  fzdifsuc2  46269  stoweidlem34  46988  subsalsal  47313  iundjiunlem  47413  iundjiun  47414  meaiuninc  47435  carageniuncllem1  47475  carageniuncl  47477  hspdifhsp  47570