ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  inteqd Unicode version

Theorem inteqd 3783
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 3781 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 14 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1332   |^|cint 3778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-int 3779
This theorem is referenced by:  intprg  3811  op1stbg  4407  onsucmin  4430  elreldm  4772  elxp5  5034  fniinfv  5486  1stval2  6060  2ndval2  6061  fundmen  6707  xpsnen  6722  fiintim  6824  elfi2  6867  fi0  6870  cardcl  7053  isnumi  7054  cardval3ex  7057  carden2bex  7061  clsfval  12307  clsval  12317
  Copyright terms: Public domain W3C validator