MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq12d Structured version   Visualization version   GIF version

Theorem difeq12d 4103
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
StepHypRef Expression
1 difeq12d.1 . . 3 (𝜑𝐴 = 𝐵)
21difeq1d 4101 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 difeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43difeq2d 4102 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2859 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1536  cdif 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3150  df-dif 3942
This theorem is referenced by:  boxcutc  8508  unfilem3  8787  infdifsn  9123  cantnfp1lem3  9146  isf32lem6  9783  isf32lem7  9784  isf32lem8  9785  domtriomlem  9867  domtriom  9868  alephsuc3  10005  symgfixelsi  18566  pmtrprfval  18618  dprdf1o  19157  isirred  19452  isdrng  19509  isdrngd  19530  drngpropd  19532  issubdrg  19563  subdrgint  19585  islbs  19851  lbspropd  19874  lssacsex  19919  lspsnat  19920  frlmlbs  20944  islindf  20959  lindfmm  20974  lsslindf  20977  ptcld  22224  iundisj  24152  iundisj2  24153  iunmbl  24157  volsup  24160  dchrval  25813  nbgrval  27121  nbgr1vtx  27143  iundisjf  30342  iundisj2f  30343  iundisjfi  30522  iundisj2fi  30523  lindfpropd  30946  sradrng  30992  qtophaus  31104  zrhunitpreima  31223  meascnbl  31482  brae  31504  braew  31505  ballotlemfrc  31788  reprdifc  31902  chtvalz  31904  satffunlem2lem2  32657  csbdif  34610  poimirlem4  34900  poimirlem6  34902  poimirlem7  34903  poimirlem9  34905  poimirlem13  34909  poimirlem14  34910  poimirlem16  34912  poimirlem19  34915  voliunnfl  34940  itg2addnclem  34947  isdivrngo  35232  drngoi  35233  lsatset  36130  watfvalN  37132  mapdpglem26  38838  mapdpglem27  38839  hvmapffval  38898  hvmapfval  38899  hvmap1o2  38905  prjspval  39259  dssmapfvd  40369  fzdifsuc2  41583  stoweidlem34  42326  subsalsal  42649  iundjiunlem  42748  iundjiun  42749  meaiuninc  42770  carageniuncllem1  42810  carageniuncl  42812  hspdifhsp  42905
  Copyright terms: Public domain W3C validator