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

Theorem inteqd 3867
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 3865 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 15 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   |^|cint 3862
This theorem is referenced by:  intprg  3896  ordintdif  4441  onsucmin  4612  elreldm  4903  elxp5  5161  fniinfv  5581  1stval2  6137  2ndval2  6138  fundmen  6934  xpsnen  6946  unblem2  7110  unblem3  7111  fiint  7133  elfi2  7168  fi0  7173  elfiun  7183  tcvalg  7423  tz9.12lem3  7461  rankvalb  7469  rankvalg  7489  ranksnb  7499  rankonidlem  7500  cardval3  7585  cardidm  7592  cfval  7873  cflim3  7888  coftr  7899  isfin3ds  7955  fin23lem17  7964  fin23lem39  7976  isf33lem  7992  isf34lem5  8004  isf34lem6  8006  wuncval  8364  tskmval  8461  xpnnenOLD  12488  mrcfval  13510  mrcval  13512  cycsubg2  14654  efgval  15026  lspfval  15730  lspval  15732  lsppropd  15775  aspval  16068  aspval2  16086  clsfval  16762  clsval  16774  clsval2  16787  hauscmplem  17133  cmpfi  17135  1stcfb  17171  fclscmp  17725  spanval  21912  chsupid  21991  sigagenval  23501  kur14  23747  dfrtrcl2  24045  moec  25047  istopx  25547  istopxc  25548  indcls2  25996  igenval  26686  mzpval  26810  dnnumch3lem  27143  aomclem8  27159  rgspnval  27373  iotain  27617  pclfvalN  30078  pclvalN  30079  diaintclN  31248  docaffvalN  31311  docafvalN  31312  docavalN  31313  dibintclN  31357  dihglb2  31532  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-int 3863
  Copyright terms: Public domain W3C validator