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

Theorem ineq1i 3543
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 3540 . 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 1369    i^i cin 3322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330
This theorem is referenced by:  in12  3556  inindi  3562  dfrab3  3620  dfif5  3800  disjpr2  3933  resres  5118  imainrect  5274  fresaun  5577  fresaunres2  5578  ssenen  7477  hartogslem1  7748  leiso  12204  f1oun2prg  12519  smumul  13681  firest  14363  lsmdisj2r  16173  frgpuplem  16260  ltbwe  17529  tgrest  18738  fiuncmp  18982  ptclsg  19163  metnrmlem3  20412  mbfid  21089  ppi1  22477  cht1  22478  ppiub  22518  cusgrasizeindslem2  23333  chdmj2i  24836  chjassi  24840  pjoml2i  24939  pjoml4i  24941  cmcmlem  24945  mayetes3i  25084  cvmdi  25679  atomli  25737  atabsi  25756  imadifxp  25890  gtiso  25947  prsss  26298  ordtrestNEW  26303  ordtrest2NEW  26305  esumnul  26454  measinblem  26586  eulerpartlemt  26706  ballotlem2  26823  ballotlemfp1  26826  ballotlemfval0  26830  predidm  27600  dffv5  27906  mblfinlem2  28382  ismblfin  28385  mbfposadd  28392  itg2addnclem2  28397  asindmre  28432  diophrw  29050  dnwech  29354  lmhmlnmsplit  29393
  Copyright terms: Public domain W3C validator