Theorem difeq12d 4083

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

Syntax hints:   → wi 4   = wceq 1570   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-dif 3909

This theorem is referenced by:  csbdif  4487  xpord2pred  8142  xpord3pred  8149  boxcutc  8940  unfilem3  9268  infdifsn  9627  cantnfp1lem3  9650  isf32lem6  10343  isf32lem7  10344  isf32lem8  10345  domtriomlem  10427  domtriom  10428  alephsuc3  10566  symgfixelsi  19506  pmtrprfval  19558  dprdf1o  20105  isirred  20502  isdrng  20818  isdrngd  20850  isdrngdOLD  20852  drngpropd  20854  issubdrg  20864  subdrgint  20887  islbs  21178  lbspropd  21201  lssacsex  21249  lspsnat  21250  frlmlbs  21928  islindf  21943  lindfmm  21958  lsslindf  21961  psdmullem  22309  ptcld  23751  iundisj  25688  iundisj2  25689  iunmbl  25693  volsup  25696  dchrval  27379  newval  28009  ltslpss  28082  leslss  28083  nbgrval  29667  nbgr1vtx  29689  iundisjf  32915  iundisj2f  32916  iundisjfi  33122  iundisj2fi  33123  lindfpropd  33676  opprqusdrng  33756  rprmval  33787  isufd  33811  sradrng  33953  qtophaus  34207  zrhunitpreima  34347  meascnbl  34590  brae  34612  braew  34613  ballotlemfrc  34898  reprdifc  34995  chtvalz  34997  onvf1odlem3  35570  satffunlem2lem2  35879  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem9  38261  poimirlem13  38265  poimirlem14  38266  poimirlem16  38268  poimirlem19  38271  voliunnfl  38296  itg2addnclem  38303  isdivrngo  38582  drngoi  38583  lsatset  39745  watfvalN  40747  mapdpglem26  42453  mapdpglem27  42454  hvmapffval  42513  hvmapfval  42514  hvmap1o2  42520  prjspval  43318  prjspnvs  43335  cantnfresb  44034  tfsconcatun  44047  tfsconcat0i  44055  dssmapfvd  44726  fzdifsuc2  46012  stoweidlem34  46731  subsalsal  47056  iundjiunlem  47156  iundjiun  47157  meaiuninc  47178  carageniuncllem1  47218  carageniuncl  47220  hspdifhsp  47313