Theorem difeq12d 3880

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

Syntax hints:   → wi 4   = wceq 1631   ∖ cdif 3720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-dif 3726

This theorem is referenced by:  boxcutc  8108  unfilem3  8385  infdifsn  8721  cantnfp1lem3  8744  infcda1  9220  isf32lem6  9385  isf32lem7  9386  isf32lem8  9387  domtriomlem  9469  domtriom  9470  alephsuc3  9607  symgfixelsi  18061  pmtrprfval  18113  dprdf1o  18638  isirred  18906  isdrng  18960  isdrngd  18981  drngpropd  18983  issubdrg  19014  islbs  19288  lbspropd  19311  lssacsex  19357  lspsnat  19358  frlmlbs  20352  islindf  20367  lindfmm  20382  lsslindf  20385  ptcld  21636  iundisj  23535  iundisj2  23536  iunmbl  23540  volsup  23543  dchrval  25179  nbgrval  26451  nbgr1vtx  26476  iundisjf  29739  iundisj2f  29740  iundisjfi  29894  iundisj2fi  29895  qtophaus  30242  zrhunitpreima  30361  meascnbl  30621  brae  30643  braew  30644  ballotlemfrc  30927  reprdifc  31044  chtvalz  31046  csbdif  33507  poimirlem4  33745  poimirlem6  33747  poimirlem7  33748  poimirlem9  33750  poimirlem13  33754  poimirlem14  33755  poimirlem16  33757  poimirlem19  33760  voliunnfl  33785  itg2addnclem  33792  isdivrngo  34080  drngoi  34081  lsatset  34798  watfvalN  35800  mapdpglem26  37508  mapdpglem27  37509  hvmapffval  37568  hvmapfval  37569  hvmap1o2  37575  dssmapfvd  38837  fzdifsuc2  40038  stoweidlem34  40765  subsalsal  41091  iundjiunlem  41190  iundjiun  41191  meaiuninc  41212  carageniuncllem1  41252  carageniuncl  41254  hspdifhsp  41347