Theorem difeq12d 4084

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

Syntax hints:   → wi 4   = wceq 1563   ∖ cdif 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-dif 3910

This theorem is referenced by:  csbdif  4482  xpord2pred  8129  xpord3pred  8136  boxcutc  8927  unfilem3  9255  infdifsn  9614  cantnfp1lem3  9637  isf32lem6  10330  isf32lem7  10331  isf32lem8  10332  domtriomlem  10414  domtriom  10415  alephsuc3  10553  symgfixelsi  19496  pmtrprfval  19548  dprdf1o  20095  isirred  20492  isdrng  20808  isdrngd  20838  isdrngdOLD  20840  drngpropd  20842  issubdrg  20852  subdrgint  20875  islbs  21166  lbspropd  21189  lssacsex  21237  lspsnat  21238  frlmlbs  21907  islindf  21922  lindfmm  21937  lsslindf  21940  psdmullem  22288  ptcld  23731  iundisj  25668  iundisj2  25669  iunmbl  25673  volsup  25676  dchrval  27356  newval  27986  ltslpss  28059  leslss  28060  nbgrval  29595  nbgr1vtx  29617  iundisjf  32844  iundisj2f  32845  iundisjfi  33053  iundisj2fi  33054  lindfpropd  33611  opprqusdrng  33692  rprmval  33723  isufd  33747  sradrng  33889  qtophaus  34143  zrhunitpreima  34283  meascnbl  34526  brae  34548  braew  34549  ballotlemfrc  34834  reprdifc  34931  chtvalz  34933  onvf1odlem3  35460  satffunlem2lem2  35769  poimirlem4  38135  poimirlem6  38137  poimirlem7  38138  poimirlem9  38140  poimirlem13  38144  poimirlem14  38145  poimirlem16  38147  poimirlem19  38150  voliunnfl  38175  itg2addnclem  38182  isdivrngo  38461  drngoi  38462  lsatset  39626  watfvalN  40628  mapdpglem26  42334  mapdpglem27  42335  hvmapffval  42394  hvmapfval  42395  hvmap1o2  42401  prjspval  43197  prjspnvs  43214  cantnfresb  43913  tfsconcatun  43926  tfsconcat0i  43934  dssmapfvd  44605  fzdifsuc2  45887  stoweidlem34  46606  subsalsal  46931  iundjiunlem  47031  iundjiun  47032  meaiuninc  47053  carageniuncllem1  47093  carageniuncl  47095  hspdifhsp  47188