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

Theorem ineq1i 3538
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 3535 . 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 1652    i^i cin 3319
This theorem is referenced by:  in12  3552  inindi  3558  dfrab2  3616  dfrab3  3617  dfif5  3751  disjpr2  3870  resres  5159  imainrect  5312  fresaun  5614  fresaunres2  5615  ssenen  7281  hartogslem1  7511  leiso  11708  f1oun2prg  11864  smumul  13005  firest  13660  lsmdisj2r  15317  frgpuplem  15404  ltbwe  16533  tgrest  17223  fiuncmp  17467  ptclsg  17647  metnrmlem3  18891  mbfid  19528  ppi1  20947  cht1  20948  ppiub  20988  cusgrasizeindslem2  21483  chdmj2i  22984  chjassi  22988  pjoml2i  23087  pjoml4i  23089  cmcmlem  23093  mayetes3i  23232  cvmdi  23827  atomli  23885  atabsi  23904  imadifxp  24038  gtiso  24088  esumnul  24443  measinblem  24574  ballotlem2  24746  ballotlemfp1  24749  ballotlemfval0  24753  predidm  25463  dffv5  25769  mblfinlem2  26244  ismblfin  26247  mbfposadd  26254  itg2addnclem2  26257  diophrw  26817  dnwech  27123  lmhmlnmsplit  27162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327
  Copyright terms: Public domain W3C validator