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

Theorem inteqd 4121
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 4119 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 16 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   |^|cint 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-int 4117
This theorem is referenced by:  intprg  4150  ordintdif  4755  elreldm  5051  fniinfv  5738  onsucmin  6421  elxp5  6512  1stval2  6583  2ndval2  6584  fundmen  7371  xpsnen  7383  unblem2  7553  unblem3  7554  fiint  7576  elfi2  7652  fi0  7658  elfiun  7668  tcvalg  7946  tz9.12lem3  7984  rankvalb  7992  rankvalg  8012  ranksnb  8022  rankonidlem  8023  cardval3  8110  cardidm  8117  cfval  8404  cflim3  8419  coftr  8430  isfin3ds  8486  fin23lem17  8495  fin23lem39  8507  isf33lem  8523  isf34lem5  8535  isf34lem6  8537  wuncval  8897  tskmval  8994  xpnnenOLD  13475  mrcfval  14529  mrcval  14531  cycsubg2  15698  efgval  16194  lspfval  16976  lspval  16978  lsppropd  17021  aspval  17321  aspval2  17339  clsfval  18471  clsval  18483  clsval2  18496  hauscmplem  18851  cmpfi  18853  1stcfb  18891  fclscmp  19445  spanval  24559  chsupid  24638  sigagenval  26437  kur14  26952  dfrtrcl2  27197  igenval  28705  mzpval  28913  dnnumch3lem  29244  aomclem8  29259  rgspnval  29370  iotain  29516  pclfvalN  33106  pclvalN  33107  diaintclN  34276  docaffvalN  34339  docafvalN  34340  docavalN  34341  dibintclN  34385  dihglb2  34560  dihintcl  34562
  Copyright terms: Public domain W3C validator