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

Theorem ineq1i 3442
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Hypothesis
Ref Expression
ineq1i.1  |-  A  =  B
Assertion
Ref Expression
ineq1i  |-  ( A  i^i  C )  =  ( B  i^i  C
)

Proof of Theorem ineq1i
StepHypRef Expression
1 ineq1i.1 . 2  |-  A  =  B
2 ineq1 3439 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
31, 2ax-mp 8 1  |-  ( A  i^i  C )  =  ( B  i^i  C
)
Colors of variables: wff set class
Syntax hints:    = wceq 1642    i^i cin 3227
This theorem is referenced by:  in12  3456  inindi  3462  dfrab2  3519  dfrab3  3520  dfif5  3653  resres  5047  imainrect  5198  fresaun  5492  fresaunres2  5493  ssenen  7120  hartogslem1  7344  leiso  11487  smumul  12775  firest  13430  lsmdisj2r  15087  frgpuplem  15174  ltbwe  16307  tgrest  16990  fiuncmp  17231  ptclsg  17409  metnrmlem3  18462  mbfid  19089  ppi1  20508  cht1  20509  ppiub  20549  chdmj2i  22169  chjassi  22173  pjoml2i  22272  pjoml4i  22274  cmcmlem  22278  mayetes3i  22417  cvmdi  23012  atomli  23070  atabsi  23089  imadifxp  23238  gtiso  23289  esumnul  23709  measinblem  23838  ballotlem2  23995  ballotlemfp1  23998  ballotlemfval0  24002  predidm  24746  dffv5  25021  itg2addnclem2  25493  diophrw  26161  dnwech  26468  lmhmlnmsplit  26508  disjpr2  27409  f1oun2prg  27421  cusgrasizeindslem2  27629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235
  Copyright terms: Public domain W3C validator