Theorem difeq12d 3729

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

Syntax hints:   → wi 4   = wceq 1483   ∖ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-dif 3577

This theorem is referenced by:  boxcutc  7951  unfilem3  8226  infdifsn  8554  cantnfp1lem3  8577  infcda1  9015  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  domtriomlem  9264  domtriom  9265  alephsuc3  9402  symgfixelsi  17855  pmtrprfval  17907  dprdf1o  18431  isirred  18699  isdrng  18751  isdrngd  18772  drngpropd  18774  issubdrg  18805  islbs  19076  lbspropd  19099  lssacsex  19144  lspsnat  19145  frlmlbs  20136  islindf  20151  lindfmm  20166  lsslindf  20169  ptcld  21416  iundisj  23316  iundisj2  23317  iunmbl  23321  volsup  23324  dchrval  24959  nbgrval  26234  nbgr1vtx  26254  iundisjf  29402  iundisj2f  29403  iundisjfi  29555  iundisj2fi  29556  qtophaus  29903  zrhunitpreima  30022  meascnbl  30282  brae  30304  braew  30305  ballotlemfrc  30588  reprdifc  30705  chtvalz  30707  csbdif  33171  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem19  33428  voliunnfl  33453  itg2addnclem  33461  isdivrngo  33749  drngoi  33750  lsatset  34277  watfvalN  35278  mapdpglem26  36987  mapdpglem27  36988  hvmapffval  37047  hvmapfval  37048  hvmap1o2  37054  dssmapfvd  38311  fzdifsuc2  39525  stoweidlem34  40251  subsalsal  40577  iundjiunlem  40676  iundjiun  40677  meaiuninc  40698  carageniuncllem1  40735  carageniuncl  40737  hspdifhsp  40830