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

Theorem inteqd 4252
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 4250 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 17 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454   |^|cint 4247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-int 4248
This theorem is referenced by:  intprg  4282  elreldm  5077  ordintdif  5490  fniinfv  5946  onsucmin  6674  elxp5  6764  1stval2  6836  2ndval2  6837  fundmen  7668  xpsnen  7681  unblem2  7849  unblem3  7850  fiint  7873  elfi2  7953  fi0  7959  elfiun  7969  tcvalg  8247  tz9.12lem3  8285  rankvalb  8293  rankvalg  8313  ranksnb  8323  rankonidlem  8324  cardval3  8411  cardidm  8418  cfval  8702  cflim3  8717  coftr  8728  isfin3ds  8784  fin23lem17  8793  fin23lem39  8805  isf33lem  8821  isf34lem5  8833  isf34lem6  8835  wuncval  9192  tskmval  9289  cleq1  13095  dfrtrcl2  13173  mrcfval  15562  mrcval  15564  cycsubg2  16902  efgval  17415  lspfval  18244  lspval  18246  lsppropd  18289  aspval  18600  aspval2  18619  clsfval  20088  clsval  20100  clsval2  20113  hauscmplem  20469  cmpfi  20471  1stcfb  20508  fclscmp  21093  spanval  27034  chsupid  27113  sigagenval  29010  kur14  29987  mclsval  30249  igenval  32338  pclfvalN  33498  pclvalN  33499  diaintclN  34670  docaffvalN  34733  docafvalN  34734  docavalN  34735  dibintclN  34779  dihglb2  34954  dihintcl  34956  mzpval  35618  dnnumch3lem  35948  aomclem8  35963  rgspnval  36078  iotain  36811  salgenval  38219
  Copyright terms: Public domain W3C validator