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

Theorem ineq1i 3366
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 3363 . 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 1623    i^i cin 3151
This theorem is referenced by:  in12  3380  inindi  3386  dfrab2  3443  dfrab3  3444  dfif5  3577  resres  4968  imainrect  5119  fresaun  5412  fresaunres2  5413  ssenen  7035  hartogslem1  7257  leiso  11397  smumul  12684  firest  13337  lsmdisj2r  14994  frgpuplem  15081  ltbwe  16214  tgrest  16890  fiuncmp  17131  ptclsg  17309  metnrmlem3  18365  mbfid  18991  ppi1  20402  cht1  20403  ppiub  20443  chdmj2i  22061  chjassi  22065  pjoml2i  22164  pjoml4i  22166  cmcmlem  22170  mayetes3i  22309  cvmdi  22904  atomli  22962  atabsi  22981  ballotlem2  23047  ballotlemfp1  23050  ballotlemfval0  23054  gtiso  23241  esumnul  23427  measinblem  23547  predidm  24188  dffv5  24463  inposet  25278  selsubf  25990  selsubf3  25991  diophrw  26838  dnwech  27145  lmhmlnmsplit  27185  f1oun2prg  28076
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-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator