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

Theorem ineq1i 3649
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 3646 . 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 1370    i^i cin 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-in 3436
This theorem is referenced by:  in12  3662  inindi  3668  dfrab3  3726  dfif5  3906  disjpr2  4039  resres  5224  imainrect  5380  fresaun  5683  fresaunres2  5684  ssenen  7588  hartogslem1  7860  leiso  12323  f1oun2prg  12638  smumul  13800  firest  14482  lsmdisj2r  16295  frgpuplem  16382  ltbwe  17670  tgrest  18888  fiuncmp  19132  ptclsg  19313  metnrmlem3  20562  mbfid  21240  ppi1  22628  cht1  22629  ppiub  22669  cusgrasizeindslem2  23527  chdmj2i  25030  chjassi  25034  pjoml2i  25133  pjoml4i  25135  cmcmlem  25139  mayetes3i  25278  cvmdi  25873  atomli  25931  atabsi  25950  imadifxp  26083  gtiso  26140  prsss  26484  ordtrestNEW  26489  ordtrest2NEW  26491  esumnul  26640  measinblem  26772  eulerpartlemt  26891  ballotlem2  27008  ballotlemfp1  27011  ballotlemfval0  27015  predidm  27786  dffv5  28092  mblfinlem2  28570  ismblfin  28573  mbfposadd  28580  itg2addnclem2  28585  asindmre  28620  diophrw  29238  dnwech  29542  lmhmlnmsplit  29581
  Copyright terms: Public domain W3C validator