Theorem difeq12d 4100

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-dif 3939

This theorem is referenced by:  boxcutc  8505  unfilem3  8784  infdifsn  9120  cantnfp1lem3  9143  isf32lem6  9780  isf32lem7  9781  isf32lem8  9782  domtriomlem  9864  domtriom  9865  alephsuc3  10002  symgfixelsi  18563  pmtrprfval  18615  dprdf1o  19154  isirred  19449  isdrng  19506  isdrngd  19527  drngpropd  19529  issubdrg  19560  subdrgint  19582  islbs  19848  lbspropd  19871  lssacsex  19916  lspsnat  19917  frlmlbs  20941  islindf  20956  lindfmm  20971  lsslindf  20974  ptcld  22221  iundisj  24149  iundisj2  24150  iunmbl  24154  volsup  24157  dchrval  25810  nbgrval  27118  nbgr1vtx  27140  iundisjf  30339  iundisj2f  30340  iundisjfi  30519  iundisj2fi  30520  lindfpropd  30942  sradrng  30988  qtophaus  31100  zrhunitpreima  31219  meascnbl  31478  brae  31500  braew  31501  ballotlemfrc  31784  reprdifc  31898  chtvalz  31900  satffunlem2lem2  32653  csbdif  34609  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem9  34916  poimirlem13  34920  poimirlem14  34921  poimirlem16  34923  poimirlem19  34926  voliunnfl  34951  itg2addnclem  34958  isdivrngo  35243  drngoi  35244  lsatset  36141  watfvalN  37143  mapdpglem26  38849  mapdpglem27  38850  hvmapffval  38909  hvmapfval  38910  hvmap1o2  38916  prjspval  39302  dssmapfvd  40412  fzdifsuc2  41626  stoweidlem34  42368  subsalsal  42691  iundjiunlem  42790  iundjiun  42791  meaiuninc  42812  carageniuncllem1  42852  carageniuncl  42854  hspdifhsp  42947