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

Theorem inteqd 3991
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 3989 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 16 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   |^|cint 3986
This theorem is referenced by:  intprg  4020  ordintdif  4565  onsucmin  4735  elreldm  5028  elxp5  5292  fniinfv  5718  1stval2  6297  2ndval2  6298  fundmen  7110  xpsnen  7122  unblem2  7290  unblem3  7291  fiint  7313  elfi2  7348  fi0  7354  elfiun  7364  tcvalg  7604  tz9.12lem3  7642  rankvalb  7650  rankvalg  7670  ranksnb  7680  rankonidlem  7681  cardval3  7766  cardidm  7773  cfval  8054  cflim3  8069  coftr  8080  isfin3ds  8136  fin23lem17  8145  fin23lem39  8157  isf33lem  8173  isf34lem5  8185  isf34lem6  8187  wuncval  8544  tskmval  8641  xpnnenOLD  12730  mrcfval  13754  mrcval  13756  cycsubg2  14898  efgval  15270  lspfval  15970  lspval  15972  lsppropd  16015  aspval  16308  aspval2  16326  clsfval  17006  clsval  17018  clsval2  17031  hauscmplem  17385  cmpfi  17387  1stcfb  17423  fclscmp  17977  spanval  22677  chsupid  22756  sigagenval  24313  kur14  24675  dfrtrcl2  24921  igenval  26356  mzpval  26474  dnnumch3lem  26806  aomclem8  26822  rgspnval  27036  iotain  27280  pclfvalN  30055  pclvalN  30056  diaintclN  31225  docaffvalN  31288  docafvalN  31289  docavalN  31290  dibintclN  31334  dihglb2  31509  dihintcl  31511
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ral 2648  df-int 3987
  Copyright terms: Public domain W3C validator