Theorem difeq12d 4063

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-dif 3895

This theorem is referenced by:  csbdif  4464  boxcutc  8710  unfilem3  9056  infdifsn  9391  cantnfp1lem3  9414  isf32lem6  10113  isf32lem7  10114  isf32lem8  10115  domtriomlem  10197  domtriom  10198  alephsuc3  10335  symgfixelsi  19039  pmtrprfval  19091  dprdf1o  19631  isirred  19937  isdrng  19991  isdrngd  20012  drngpropd  20014  issubdrg  20045  subdrgint  20067  islbs  20334  lbspropd  20357  lssacsex  20402  lspsnat  20403  frlmlbs  21000  islindf  21015  lindfmm  21030  lsslindf  21033  ptcld  22760  iundisj  24708  iundisj2  24709  iunmbl  24713  volsup  24716  dchrval  26378  nbgrval  27699  nbgr1vtx  27721  iundisjf  30922  iundisj2f  30923  iundisjfi  31111  iundisj2fi  31112  lindfpropd  31570  rprmval  31658  sradrng  31667  qtophaus  31780  zrhunitpreima  31922  meascnbl  32181  brae  32203  braew  32204  ballotlemfrc  32487  reprdifc  32601  chtvalz  32603  satffunlem2lem2  33362  xpord2pred  33786  xpord3pred  33792  newval  34033  sltlpss  34081  poimirlem4  35775  poimirlem6  35777  poimirlem7  35778  poimirlem9  35780  poimirlem13  35784  poimirlem14  35785  poimirlem16  35787  poimirlem19  35790  voliunnfl  35815  itg2addnclem  35822  isdivrngo  36102  drngoi  36103  lsatset  36998  watfvalN  38000  mapdpglem26  39706  mapdpglem27  39707  hvmapffval  39766  hvmapfval  39767  hvmap1o2  39773  prjspval  40437  prjspnvs  40454  dssmapfvd  41593  fzdifsuc2  42818  stoweidlem34  43544  subsalsal  43867  iundjiunlem  43966  iundjiun  43967  meaiuninc  43988  carageniuncllem1  44028  carageniuncl  44030  hspdifhsp  44123