Theorem difeq12d 4090

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-dif 3917

This theorem is referenced by:  csbdif  4487  xpord2pred  8124  xpord3pred  8131  boxcutc  8914  unfilem3  9256  infdifsn  9610  cantnfp1lem3  9633  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  domtriomlem  10395  domtriom  10396  alephsuc3  10533  symgfixelsi  19365  pmtrprfval  19417  dprdf1o  19964  isirred  20328  isdrng  20642  isdrngd  20674  isdrngdOLD  20676  drngpropd  20678  issubdrg  20689  subdrgint  20712  islbs  20983  lbspropd  21006  lssacsex  21054  lspsnat  21055  frlmlbs  21706  islindf  21721  lindfmm  21736  lsslindf  21739  psdmullem  22052  ptcld  23500  iundisj  25449  iundisj2  25450  iunmbl  25454  volsup  25457  dchrval  27145  newval  27763  sltlpss  27819  slelss  27820  nbgrval  29263  nbgr1vtx  29285  iundisjf  32518  iundisj2f  32519  iundisjfi  32719  iundisj2fi  32720  lindfpropd  33353  opprqusdrng  33464  rprmval  33487  isufd  33511  sradrng  33578  qtophaus  33826  zrhunitpreima  33966  meascnbl  34209  brae  34231  braew  34232  ballotlemfrc  34518  reprdifc  34618  chtvalz  34620  onvf1odlem3  35092  satffunlem2lem2  35393  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem19  37633  voliunnfl  37658  itg2addnclem  37665  isdivrngo  37944  drngoi  37945  lsatset  38983  watfvalN  39986  mapdpglem26  41692  mapdpglem27  41693  hvmapffval  41752  hvmapfval  41753  hvmap1o2  41759  prjspval  42591  prjspnvs  42608  cantnfresb  43313  tfsconcatun  43326  tfsconcat0i  43334  dssmapfvd  44006  fzdifsuc2  45308  stoweidlem34  46032  subsalsal  46357  iundjiunlem  46457  iundjiun  46458  meaiuninc  46479  carageniuncllem1  46519  carageniuncl  46521  hspdifhsp  46614