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

Theorem ineq2 3377
Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
ineq2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )

Proof of Theorem ineq2
StepHypRef Expression
1 ineq1 3376 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
2 incom 3374 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3374 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33eqtr4g 2353 1  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    i^i cin 3164
This theorem is referenced by:  ineq12  3378  ineq2i  3380  ineq2d  3383  uneqin  3433  intprg  3912  wefrc  4403  onfr  4447  onnseq  6377  qsdisj  6752  disjenex  7035  fiint  7149  elfiun  7199  dffi3  7200  cplem2  7576  dfac5  7771  kmlem2  7793  kmlem13  7804  kmlem14  7805  ackbij1lem16  7877  fin23lem12  7973  fin23lem19  7978  fin23lem33  7987  uzin2  11844  pgpfac1lem3  15328  pgpfac1lem5  15330  pgpfac1  15331  inopn  16661  basis1  16704  basis2  16705  baspartn  16708  fctop  16757  cctop  16759  ordtbaslem  16934  hausnei2  17097  cnhaus  17098  nrmsep  17101  isnrm2  17102  dishaus  17126  ordthauslem  17127  dfcon2  17161  nconsubb  17165  kgeni  17248  pthaus  17348  txhaus  17357  xkohaus  17363  regr1lem  17446  fbasssin  17547  fbun  17551  fbunfip  17580  filcon  17594  isufil2  17619  ufileu  17630  filufint  17631  fmfnfmlem4  17668  fmfnfm  17669  fclsopni  17726  fclsbas  17732  fclsrest  17735  isfcf  17745  tsmsfbas  17826  metreslem  17942  methaus  18082  qtopbaslem  18283  metnrmlem3  18381  ismbl  18901  shincl  21976  chincl  22094  chdmm1  22120  ledi  22135  cmbr  22179  cmbr3i  22195  cmbr3  22203  pjoml2  22206  stcltrlem1  22872  mdbr  22890  dmdbr  22895  cvmd  22932  cvexch  22970  sumdmdii  23011  mddmdin0i  23027  ballotlemfval  23064  ballotlemgval  23098  cvmscbv  23804  cvmsdisj  23816  cvmsss2  23820  nepss  24087  neiopne  25154  basexre  25625  bwt2  25695  hdrmp  25809  isibg2aa  26215  isibg2aalem3  26218  isside0  26267  finlocfin  26402  locfindis  26408  tailfb  26429  elrfi  26872  csbresgVD  28987  lshpinN  29801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator