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

Theorem ineq1i 3641
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 3638 . 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 1454    i^i cin 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422
This theorem is referenced by:  in12  3654  inindi  3660  dfrab3  3729  dfif5  3908  disjpr2  4045  resres  5135  imainrect  5296  predidm  5420  fresaun  5776  fresaunres2  5777  ssenen  7771  hartogslem1  8082  leiso  12654  f1oun2prg  13047  smumul  14515  firest  15379  lsmdisj2r  17383  frgpuplem  17470  ltbwe  18744  tgrest  20223  fiuncmp  20467  ptclsg  20678  metnrmlem3  21926  metnrmlem3OLD  21941  mbfid  22640  ppi1  24139  cht1  24140  ppiub  24180  cusgrasizeindslem2  25250  chdmj2i  27183  chjassi  27187  pjoml2i  27286  pjoml4i  27288  cmcmlem  27292  mayetes3i  27430  cvmdi  28025  atomli  28083  atabsi  28102  uniin1  28212  disjuniel  28255  imadifxp  28260  gtiso  28329  prsss  28770  ordtrest2NEW  28777  esumnul  28917  measinblem  29090  eulerpartlemt  29252  ballotlem2  29369  ballotlemfp1  29372  ballotlemfval0  29376  mthmpps  30268  dffv5  30739  mblfinlem2  32022  ismblfin  32025  mbfposadd  32032  itg2addnclem2  32038  asindmre  32071  diophrw  35645  dnwech  35950  lmhmlnmsplit  35989  rp-fakeuninass  36205  iunrelexp0  36338  nznngen  36708  sge0sn  38258  prinfzo0  39107
  Copyright terms: Public domain W3C validator