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

Theorem difeq12d 3712
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 3710 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 difeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43difeq2d 3711 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2655 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cdif 3556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-dif 3562
This theorem is referenced by:  boxcutc  7903  unfilem3  8178  infdifsn  8506  cantnfp1lem3  8529  infcda1  8967  isf32lem6  9132  isf32lem7  9133  isf32lem8  9134  domtriomlem  9216  domtriom  9217  alephsuc3  9354  symgfixelsi  17787  pmtrprfval  17839  dprdf1o  18363  isirred  18631  isdrng  18683  isdrngd  18704  drngpropd  18706  issubdrg  18737  islbs  19008  lbspropd  19031  lssacsex  19076  lspsnat  19077  frlmlbs  20068  islindf  20083  lindfmm  20098  lsslindf  20101  ptcld  21339  iundisj  23239  iundisj2  23240  iunmbl  23244  volsup  23247  dchrval  24876  nbgrval  26138  nbgr1vtx  26158  iundisjf  29270  iundisj2f  29271  iundisjfi  29420  iundisj2fi  29421  qtophaus  29709  zrhunitpreima  29828  meascnbl  30087  brae  30109  braew  30110  ballotlemfrc  30393  csbdif  32838  poimirlem4  33080  poimirlem6  33082  poimirlem7  33083  poimirlem9  33085  poimirlem13  33089  poimirlem14  33090  poimirlem16  33092  poimirlem19  33095  voliunnfl  33120  itg2addnclem  33128  isdivrngo  33416  drngoi  33417  lsatset  33792  watfvalN  34793  mapdpglem26  36502  mapdpglem27  36503  hvmapffval  36562  hvmapfval  36563  hvmap1o2  36569  dssmapfvd  37828  fzdifsuc2  39020  stoweidlem34  39584  subsalsal  39910  iundjiunlem  40009  iundjiun  40010  meaiuninc  40031  carageniuncllem1  40068  carageniuncl  40070  hspdifhsp  40163
  Copyright terms: Public domain W3C validator