Theorem difeq12d 3927

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

Syntax hints:   → wi 4   = wceq 1653   ∖ cdif 3766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rab 3098  df-dif 3772

This theorem is referenced by:  boxcutc  8191  unfilem3  8468  infdifsn  8804  cantnfp1lem3  8827  infcda1  9303  isf32lem6  9468  isf32lem7  9469  isf32lem8  9470  domtriomlem  9552  domtriom  9553  alephsuc3  9690  symgfixelsi  18167  pmtrprfval  18219  dprdf1o  18747  isirred  19015  isdrng  19069  isdrngd  19090  drngpropd  19092  issubdrg  19123  islbs  19397  lbspropd  19420  lssacsex  19466  lspsnat  19467  frlmlbs  20461  islindf  20476  lindfmm  20491  lsslindf  20494  ptcld  21745  iundisj  23656  iundisj2  23657  iunmbl  23661  volsup  23664  dchrval  25311  nbgrval  26571  nbgr1vtx  26596  iundisjf  29919  iundisj2f  29920  iundisjfi  30073  iundisj2fi  30074  qtophaus  30419  zrhunitpreima  30538  meascnbl  30798  brae  30820  braew  30821  ballotlemfrc  31105  reprdifc  31225  chtvalz  31227  csbdif  33670  poimirlem4  33902  poimirlem6  33904  poimirlem7  33905  poimirlem9  33907  poimirlem13  33911  poimirlem14  33912  poimirlem16  33914  poimirlem19  33917  voliunnfl  33942  itg2addnclem  33949  isdivrngo  34236  drngoi  34237  lsatset  35011  watfvalN  36013  mapdpglem26  37719  mapdpglem27  37720  hvmapffval  37779  hvmapfval  37780  hvmap1o2  37786  dssmapfvd  39093  fzdifsuc2  40269  stoweidlem34  40994  subsalsal  41320  iundjiunlem  41419  iundjiun  41420  meaiuninc  41441  carageniuncllem1  41481  carageniuncl  41483  hspdifhsp  41576