MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inteqd Structured version   Unicode version

Theorem inteqd 4287
Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
inteqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
inteqd  |-  ( ph  ->  |^| A  =  |^| B )

Proof of Theorem inteqd
StepHypRef Expression
1 inteqd.1 . 2  |-  ( ph  ->  A  =  B )
2 inteq 4285 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 16 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   |^|cint 4282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-int 4283
This theorem is referenced by:  intprg  4316  ordintdif  4927  elreldm  5225  fniinfv  5924  onsucmin  6634  elxp5  6726  1stval2  6798  2ndval2  6799  fundmen  7586  xpsnen  7598  unblem2  7769  unblem3  7770  fiint  7793  elfi2  7870  fi0  7876  elfiun  7886  tcvalg  8165  tz9.12lem3  8203  rankvalb  8211  rankvalg  8231  ranksnb  8241  rankonidlem  8242  cardval3  8329  cardidm  8336  cfval  8623  cflim3  8638  coftr  8649  isfin3ds  8705  fin23lem17  8714  fin23lem39  8726  isf33lem  8742  isf34lem5  8754  isf34lem6  8756  wuncval  9116  tskmval  9213  xpnnenOLD  13800  mrcfval  14859  mrcval  14861  cycsubg2  16033  efgval  16531  lspfval  17402  lspval  17404  lsppropd  17447  aspval  17748  aspval2  17767  clsfval  19292  clsval  19304  clsval2  19317  hauscmplem  19672  cmpfi  19674  1stcfb  19712  fclscmp  20266  spanval  25927  chsupid  26006  sigagenval  27780  kur14  28300  dfrtrcl2  28546  igenval  30061  mzpval  30268  dnnumch3lem  30596  aomclem8  30611  rgspnval  30722  iotain  30902  pclfvalN  34685  pclvalN  34686  diaintclN  35855  docaffvalN  35918  docafvalN  35919  docavalN  35920  dibintclN  35964  dihglb2  36139  dihintcl  36141
  Copyright terms: Public domain W3C validator