Theorem difeq12d 4123

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

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-dif 3951

This theorem is referenced by:  csbdif  4527  xpord2pred  8130  xpord3pred  8137  boxcutc  8934  unfilem3  9311  infdifsn  9651  cantnfp1lem3  9674  isf32lem6  10352  isf32lem7  10353  isf32lem8  10354  domtriomlem  10436  domtriom  10437  alephsuc3  10574  symgfixelsi  19302  pmtrprfval  19354  dprdf1o  19901  isirred  20232  isdrng  20360  isdrngd  20389  isdrngdOLD  20391  drngpropd  20393  issubdrg  20400  subdrgint  20418  islbs  20686  lbspropd  20709  lssacsex  20756  lspsnat  20757  frlmlbs  21351  islindf  21366  lindfmm  21381  lsslindf  21384  ptcld  23116  iundisj  25064  iundisj2  25065  iunmbl  25069  volsup  25072  dchrval  26734  newval  27347  sltlpss  27398  nbgrval  28590  nbgr1vtx  28612  iundisjf  31815  iundisj2f  31816  iundisjfi  32002  iundisj2fi  32003  lindfpropd  32493  opprqusdrng  32602  rprmval  32628  sradrng  32668  qtophaus  32811  zrhunitpreima  32953  meascnbl  33212  brae  33234  braew  33235  ballotlemfrc  33520  reprdifc  33634  chtvalz  33636  satffunlem2lem2  34392  poimirlem4  36487  poimirlem6  36489  poimirlem7  36490  poimirlem9  36492  poimirlem13  36496  poimirlem14  36497  poimirlem16  36499  poimirlem19  36502  voliunnfl  36527  itg2addnclem  36534  isdivrngo  36813  drngoi  36814  lsatset  37855  watfvalN  38858  mapdpglem26  40564  mapdpglem27  40565  hvmapffval  40624  hvmapfval  40625  hvmap1o2  40631  prjspval  41346  prjspnvs  41363  cantnfresb  42064  tfsconcatun  42077  tfsconcat0i  42085  dssmapfvd  42758  fzdifsuc2  44010  stoweidlem34  44740  subsalsal  45065  iundjiunlem  45165  iundjiun  45166  meaiuninc  45187  carageniuncllem1  45227  carageniuncl  45229  hspdifhsp  45322