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

Theorem difeq12d 3762
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 3760 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 difeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43difeq2d 3761 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2685 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-dif 3610
This theorem is referenced by:  boxcutc  7993  unfilem3  8267  infdifsn  8592  cantnfp1lem3  8615  infcda1  9053  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  domtriomlem  9302  domtriom  9303  alephsuc3  9440  symgfixelsi  17901  pmtrprfval  17953  dprdf1o  18477  isirred  18745  isdrng  18799  isdrngd  18820  drngpropd  18822  issubdrg  18853  islbs  19124  lbspropd  19147  lssacsex  19192  lspsnat  19193  frlmlbs  20184  islindf  20199  lindfmm  20214  lsslindf  20217  ptcld  21464  iundisj  23362  iundisj2  23363  iunmbl  23367  volsup  23370  dchrval  25004  nbgrval  26274  nbgr1vtx  26299  iundisjf  29528  iundisj2f  29529  iundisjfi  29683  iundisj2fi  29684  qtophaus  30031  zrhunitpreima  30150  meascnbl  30410  brae  30432  braew  30433  ballotlemfrc  30716  reprdifc  30833  chtvalz  30835  csbdif  33301  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem9  33548  poimirlem13  33552  poimirlem14  33553  poimirlem16  33555  poimirlem19  33558  voliunnfl  33583  itg2addnclem  33591  isdivrngo  33879  drngoi  33880  lsatset  34595  watfvalN  35596  mapdpglem26  37304  mapdpglem27  37305  hvmapffval  37364  hvmapfval  37365  hvmap1o2  37371  dssmapfvd  38628  fzdifsuc2  39838  stoweidlem34  40569  subsalsal  40895  iundjiunlem  40994  iundjiun  40995  meaiuninc  41016  carageniuncllem1  41056  carageniuncl  41058  hspdifhsp  41151
  Copyright terms: Public domain W3C validator