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

Theorem ineq2 3549
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 3548 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
2 incom 3546 . 2  |-  ( C  i^i  A )  =  ( A  i^i  C
)
3 incom 3546 . 2  |-  ( C  i^i  B )  =  ( B  i^i  C
)
41, 2, 33eqtr4g 2500 1  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    i^i cin 3330
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 2423
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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338
This theorem is referenced by:  ineq12  3550  ineq2i  3552  ineq2d  3555  uneqin  3604  intprg  4165  wefrc  4717  onfr  4761  onnseq  6808  qsdisj  7180  disjenex  7472  fiint  7591  elfiun  7683  dffi3  7684  cplem2  8100  dfac5  8301  kmlem2  8323  kmlem13  8334  kmlem14  8335  ackbij1lem16  8407  fin23lem12  8503  fin23lem19  8508  fin23lem33  8517  uzin2  12835  pgpfac1lem3  16581  pgpfac1lem5  16583  pgpfac1  16584  inopn  18515  basis1  18558  basis2  18559  baspartn  18562  fctop  18611  cctop  18613  ordtbaslem  18795  hausnei2  18960  cnhaus  18961  nrmsep  18964  isnrm2  18965  dishaus  18989  ordthauslem  18990  bwthOLD  19017  dfcon2  19026  nconsubb  19030  kgeni  19113  pthaus  19214  txhaus  19223  xkohaus  19229  regr1lem  19315  fbasssin  19412  fbun  19416  fbunfip  19445  filcon  19459  isufil2  19484  ufileu  19495  filufint  19496  fmfnfmlem4  19533  fmfnfm  19534  fclsopni  19591  fclsbas  19597  fclsrest  19600  isfcf  19610  tsmsfbas  19701  ustincl  19785  ust0  19797  metreslem  19940  methaus  20098  qtopbaslem  20340  metnrmlem3  20440  ismbl  21012  shincl  24787  chincl  24905  chdmm1  24931  ledi  24946  cmbr  24990  cmbr3i  25006  cmbr3  25014  pjoml2  25017  stcltrlem1  25683  mdbr  25701  dmdbr  25706  cvmd  25743  cvexch  25781  sumdmdii  25822  mddmdin0i  25838  ofpreima2  25988  ballotlemfval  26875  ballotlemgval  26909  cvmscbv  27150  cvmsdisj  27162  cvmsss2  27166  nepss  27377  mblfinlem2  28432  finlocfin  28574  locfindis  28580  tailfb  28601  elrfi  29033  csbresgVD  31634  lshpinN  32637
  Copyright terms: Public domain W3C validator