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

Theorem inteqd 4047
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 4045 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 16 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   |^|cint 4042
This theorem is referenced by:  intprg  4076  ordintdif  4622  onsucmin  4793  elreldm  5086  elxp5  5350  fniinfv  5777  1stval2  6356  2ndval2  6357  fundmen  7172  xpsnen  7184  unblem2  7352  unblem3  7353  fiint  7375  elfi2  7411  fi0  7417  elfiun  7427  tcvalg  7669  tz9.12lem3  7707  rankvalb  7715  rankvalg  7735  ranksnb  7745  rankonidlem  7746  cardval3  7831  cardidm  7838  cfval  8119  cflim3  8134  coftr  8145  isfin3ds  8201  fin23lem17  8210  fin23lem39  8222  isf33lem  8238  isf34lem5  8250  isf34lem6  8252  wuncval  8609  tskmval  8706  xpnnenOLD  12801  mrcfval  13825  mrcval  13827  cycsubg2  14969  efgval  15341  lspfval  16041  lspval  16043  lsppropd  16086  aspval  16379  aspval2  16397  clsfval  17081  clsval  17093  clsval2  17106  hauscmplem  17461  cmpfi  17463  1stcfb  17500  fclscmp  18054  spanval  22827  chsupid  22906  sigagenval  24515  kur14  24894  dfrtrcl2  25140  igenval  26662  mzpval  26780  dnnumch3lem  27112  aomclem8  27127  rgspnval  27341  iotain  27585  pclfvalN  30623  pclvalN  30624  diaintclN  31793  docaffvalN  31856  docafvalN  31857  docavalN  31858  dibintclN  31902  dihglb2  32077  dihintcl  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-int 4043
  Copyright terms: Public domain W3C validator