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

Theorem ineq1i 3696
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 3693 . 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 1379    i^i cin 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483
This theorem is referenced by:  in12  3709  inindi  3715  dfrab3  3773  dfif5  3955  disjpr2  4090  resres  5284  imainrect  5446  fresaun  5754  fresaunres2  5755  ssenen  7688  hartogslem1  7963  leiso  12470  f1oun2prg  12824  smumul  13998  firest  14684  lsmdisj2r  16499  frgpuplem  16586  ltbwe  17908  tgrest  19426  fiuncmp  19670  ptclsg  19851  metnrmlem3  21100  mbfid  21778  ppi1  23166  cht1  23167  ppiub  23207  cusgrasizeindslem2  24150  chdmj2i  26076  chjassi  26080  pjoml2i  26179  pjoml4i  26181  cmcmlem  26185  mayetes3i  26324  cvmdi  26919  atomli  26977  atabsi  26996  imadifxp  27131  gtiso  27191  prsss  27534  ordtrestNEW  27539  ordtrest2NEW  27541  esumnul  27699  measinblem  27831  eulerpartlemt  27950  ballotlem2  28067  ballotlemfp1  28070  ballotlemfval0  28074  predidm  28845  dffv5  29151  mblfinlem2  29629  ismblfin  29632  mbfposadd  29639  itg2addnclem2  29644  asindmre  29679  diophrw  30296  dnwech  30598  lmhmlnmsplit  30637  nznngen  30821
  Copyright terms: Public domain W3C validator