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

Theorem ineq1i 3603
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 3600 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
31, 2ax-mp 5 1  |-  ( A  i^i  C )  =  ( B  i^i  C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    i^i cin 3378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386
This theorem is referenced by:  in12  3616  inindi  3622  dfrab3  3691  dfif5  3870  disjpr2  4005  resres  5079  imainrect  5240  predidm  5364  fresaun  5714  fresaunres2  5715  ssenen  7699  hartogslem1  8010  leiso  12570  f1oun2prg  12946  smumul  14410  firest  15274  lsmdisj2r  17278  frgpuplem  17365  ltbwe  18639  tgrest  20117  fiuncmp  20361  ptclsg  20572  metnrmlem3  21820  metnrmlem3OLD  21835  mbfid  22534  ppi1  24033  cht1  24034  ppiub  24074  cusgrasizeindslem2  25144  chdmj2i  27077  chjassi  27081  pjoml2i  27180  pjoml4i  27182  cmcmlem  27186  mayetes3i  27324  cvmdi  27919  atomli  27977  atabsi  27996  uniin1  28110  disjuniel  28153  imadifxp  28158  gtiso  28227  prsss  28674  ordtrest2NEW  28681  esumnul  28821  measinblem  28994  eulerpartlemt  29156  ballotlem2  29273  ballotlemfp1  29276  ballotlemfval0  29280  mthmpps  30172  dffv5  30640  mblfinlem2  31885  ismblfin  31888  mbfposadd  31895  itg2addnclem2  31901  asindmre  31934  diophrw  35513  dnwech  35819  lmhmlnmsplit  35858  rp-fakeuninass  36074  iunrelexp0  36207  nznngen  36578  sge0sn  38072
  Copyright terms: Public domain W3C validator