Theorem difeq12d 4065

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

Syntax hints:   → wi 4   = wceq 1547   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-dif 3893

This theorem is referenced by:  csbdif  4460  xpord2pred  8092  xpord3pred  8099  boxcutc  8886  unfilem3  9214  infdifsn  9576  cantnfp1lem3  9599  isf32lem6  10278  isf32lem7  10279  isf32lem8  10280  domtriomlem  10362  domtriom  10363  alephsuc3  10501  symgfixelsi  19408  pmtrprfval  19460  dprdf1o  20007  isirred  20397  isdrng  20712  isdrngd  20744  isdrngdOLD  20746  drngpropd  20748  issubdrg  20759  subdrgint  20782  islbs  21073  lbspropd  21096  lssacsex  21144  lspsnat  21145  frlmlbs  21779  islindf  21794  lindfmm  21809  lsslindf  21812  psdmullem  22160  ptcld  23603  iundisj  25540  iundisj2  25541  iunmbl  25545  volsup  25548  dchrval  27222  newval  27852  ltslpss  27925  leslss  27926  nbgrval  29430  nbgr1vtx  29452  iundisjf  32685  iundisj2f  32686  iundisjfi  32895  iundisj2fi  32896  lindfpropd  33472  opprqusdrng  33583  rprmval  33606  isufd  33630  sradrng  33773  qtophaus  34027  zrhunitpreima  34167  meascnbl  34410  brae  34432  braew  34433  ballotlemfrc  34718  reprdifc  34818  chtvalz  34820  onvf1odlem3  35340  satffunlem2lem2  35641  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem9  38003  poimirlem13  38007  poimirlem14  38008  poimirlem16  38010  poimirlem19  38013  voliunnfl  38038  itg2addnclem  38045  isdivrngo  38324  drngoi  38325  lsatset  39489  watfvalN  40491  mapdpglem26  42197  mapdpglem27  42198  hvmapffval  42257  hvmapfval  42258  hvmap1o2  42264  prjspval  43060  prjspnvs  43077  cantnfresb  43776  tfsconcatun  43789  tfsconcat0i  43797  dssmapfvd  44468  fzdifsuc2  45765  stoweidlem34  46484  subsalsal  46809  iundjiunlem  46909  iundjiun  46910  meaiuninc  46931  carageniuncllem1  46971  carageniuncl  46973  hspdifhsp  47066