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

Theorem ineq1i 3498
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 3495 . 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 1649    i^i cin 3279
This theorem is referenced by:  in12  3512  inindi  3518  dfrab2  3576  dfrab3  3577  dfif5  3711  disjpr2  3830  resres  5118  imainrect  5271  fresaun  5573  fresaunres2  5574  ssenen  7240  hartogslem1  7467  leiso  11663  f1oun2prg  11819  smumul  12960  firest  13615  lsmdisj2r  15272  frgpuplem  15359  ltbwe  16488  tgrest  17177  fiuncmp  17421  ptclsg  17600  metnrmlem3  18844  mbfid  19481  ppi1  20900  cht1  20901  ppiub  20941  cusgrasizeindslem2  21436  chdmj2i  22937  chjassi  22941  pjoml2i  23040  pjoml4i  23042  cmcmlem  23046  mayetes3i  23185  cvmdi  23780  atomli  23838  atabsi  23857  imadifxp  23991  gtiso  24041  esumnul  24396  measinblem  24527  ballotlem2  24699  ballotlemfp1  24702  ballotlemfval0  24706  predidm  25402  dffv5  25677  mblfinlem  26143  ismblfin  26146  mbfposadd  26153  itg2addnclem2  26156  diophrw  26707  dnwech  27013  lmhmlnmsplit  27053
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287
  Copyright terms: Public domain W3C validator