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

Theorem ineq1i 3682
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 3679 . 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 1398    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468
This theorem is referenced by:  in12  3695  inindi  3701  dfrab3  3770  dfif5  3945  disjpr2  4078  resres  5274  imainrect  5433  fresaun  5738  fresaunres2  5739  ssenen  7684  hartogslem1  7959  leiso  12492  f1oun2prg  12856  smumul  14227  firest  14922  lsmdisj2r  16902  frgpuplem  16989  ltbwe  18332  tgrest  19827  fiuncmp  20071  ptclsg  20282  metnrmlem3  21531  mbfid  22209  ppi1  23636  cht1  23637  ppiub  23677  cusgrasizeindslem2  24676  chdmj2i  26598  chjassi  26602  pjoml2i  26701  pjoml4i  26703  cmcmlem  26707  mayetes3i  26846  cvmdi  27441  atomli  27499  atabsi  27518  disjuniel  27667  imadifxp  27672  gtiso  27747  prsss  28133  ordtrest2NEW  28140  esumnul  28277  measinblem  28428  eulerpartlemt  28574  ballotlem2  28691  ballotlemfp1  28694  ballotlemfval0  28698  mthmpps  29206  predidm  29508  dffv5  29802  mblfinlem2  30292  ismblfin  30295  mbfposadd  30302  itg2addnclem2  30307  asindmre  30342  diophrw  30931  dnwech  31233  lmhmlnmsplit  31272  nznngen  31462  rp-fakeuninass  38155  iunrelexp0  38224
  Copyright terms: Public domain W3C validator