Theorem difeq12d 4054

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  csbdif  4455  boxcutc  8687  unfilem3  9010  infdifsn  9345  cantnfp1lem3  9368  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  domtriomlem  10129  domtriom  10130  alephsuc3  10267  symgfixelsi  18958  pmtrprfval  19010  dprdf1o  19550  isirred  19856  isdrng  19910  isdrngd  19931  drngpropd  19933  issubdrg  19964  subdrgint  19986  islbs  20253  lbspropd  20276  lssacsex  20321  lspsnat  20322  frlmlbs  20914  islindf  20929  lindfmm  20944  lsslindf  20947  ptcld  22672  iundisj  24617  iundisj2  24618  iunmbl  24622  volsup  24625  dchrval  26287  nbgrval  27606  nbgr1vtx  27628  iundisjf  30829  iundisj2f  30830  iundisjfi  31019  iundisj2fi  31020  lindfpropd  31478  rprmval  31566  sradrng  31575  qtophaus  31688  zrhunitpreima  31828  meascnbl  32087  brae  32109  braew  32110  ballotlemfrc  32393  reprdifc  32507  chtvalz  32509  satffunlem2lem2  33268  xpord2pred  33719  xpord3pred  33725  newval  33966  sltlpss  34014  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem13  35717  poimirlem14  35718  poimirlem16  35720  poimirlem19  35723  voliunnfl  35748  itg2addnclem  35755  isdivrngo  36035  drngoi  36036  lsatset  36931  watfvalN  37933  mapdpglem26  39639  mapdpglem27  39640  hvmapffval  39699  hvmapfval  39700  hvmap1o2  39706  prjspval  40363  prjspnvs  40380  dssmapfvd  41514  fzdifsuc2  42739  stoweidlem34  43465  subsalsal  43788  iundjiunlem  43887  iundjiun  43888  meaiuninc  43909  carageniuncllem1  43949  carageniuncl  43951  hspdifhsp  44044