Theorem difeq12d 4067

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  csbdif  4484  xpord2pred  8192  xpord3pred  8199  boxcutc  9000  unfilem3  9330  infdifsn  9688  cantnfp1lem3  9711  isf32lem6  10466  isf32lem7  10467  isf32lem8  10468  domtriomlem  10550  domtriom  10551  alephsuc3  10695  symgfixelsi  19682  pmtrprfval  19734  dprdf1o  20281  isirred  20682  isdrng  21017  isdrngd  21055  isdrngdOLD  21057  drngpropd  21060  issubdrg  21070  subdrgint  21093  islbs  21384  lbspropd  21407  lssacsex  21455  lspsnat  21456  frlmlbs  22136  islindf  22151  lindfmm  22166  lsslindf  22169  psdmullem  22519  ptcld  23965  iundisj  25902  iundisj2  25903  iunmbl  25907  volsup  25910  dchrval  27594  newval  28254  ltslpss  28327  leslss  28328  nbgrval  29950  nbgr1vtx  29972  iundisjf  33258  iundisj2f  33259  iundisjfi  33461  iundisj2fi  33462  lindfpropd  34021  opprqusdrng  34101  rprmval  34132  isufd  34156  sradrng  34297  qtophaus  34551  zrhunitpreima  34691  meascnbl  34935  brae  34957  braew  34958  ballotlemfrc  35242  reprdifc  35339  chtvalz  35341  onvf1odlem3  36046  satffunlem2lem2  36351  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem9  38752  poimirlem13  38756  poimirlem14  38757  poimirlem16  38759  poimirlem19  38762  voliunnfl  38787  itg2addnclem  38794  isdivrngo  39087  drngoi  39088  lsatset  40250  watfvalN  41252  mapdpglem26  42958  mapdpglem27  42959  hvmapffval  43018  hvmapfval  43019  hvmap1o2  43025  prjspval  43835  prjspnvs  43852  cantnfresb  44529  tfsconcatun  44542  tfsconcat0i  44550  dssmapfvd  45220  fzdifsuc2  46541  stoweidlem34  47259  subsalsal  47584  iundjiunlem  47684  iundjiun  47685  meaiuninc  47706  carageniuncllem1  47746  carageniuncl  47748  hspdifhsp  47841