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

Theorem ineq2 4133
 Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
ineq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem ineq2
StepHypRef Expression
1 ineq1 4131 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 4128 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4128 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2858 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∩ cin 3880 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888 This theorem is referenced by:  ineq12  4134  ineq2i  4136  ineq2d  4139  uneqin  4205  intprg  4872  wefrc  5513  onfr  6198  onnseq  7966  qsdisj  8359  disjenex  8661  fiint  8781  elfiun  8880  dffi3  8881  cplem2  9305  dfac5  9541  kmlem2  9564  kmlem13  9575  kmlem14  9576  ackbij1lem16  9648  fin23lem12  9744  fin23lem19  9749  fin23lem33  9758  uzin2  14698  pgpfac1lem3  19195  pgpfac1lem5  19197  pgpfac1  19198  inopn  21511  basis1  21562  basis2  21563  baspartn  21566  fctop  21616  cctop  21618  ordtbaslem  21800  hausnei2  21965  cnhaus  21966  nrmsep  21969  isnrm2  21970  dishaus  21994  ordthauslem  21995  dfconn2  22031  nconnsubb  22035  finlocfin  22132  dissnlocfin  22141  locfindis  22142  kgeni  22149  pthaus  22250  txhaus  22259  xkohaus  22265  regr1lem  22351  fbasssin  22448  fbun  22452  fbunfip  22481  filconn  22495  isufil2  22520  ufileu  22531  filufint  22532  fmfnfmlem4  22569  fmfnfm  22570  fclsopni  22627  fclsbas  22633  fclsrest  22636  isfcf  22646  tsmsfbas  22740  ustincl  22820  ust0  22832  metreslem  22976  methaus  23134  qtopbaslem  23371  metnrmlem3  23473  ismbl  24137  shincl  29171  chincl  29289  chdmm1  29315  ledi  29330  cmbr  29374  cmbr3i  29390  cmbr3  29398  pjoml2  29401  stcltrlem1  30066  mdbr  30084  dmdbr  30089  cvmd  30126  cvexch  30164  sumdmdii  30205  mddmdin0i  30221  ofpreima2  30436  crefeq  31210  ldgenpisyslem1  31544  ldgenpisys  31547  inelsros  31559  diffiunisros  31560  elcarsg  31685  carsgclctunlem2  31699  carsgclctun  31701  ballotlemfval  31869  ballotlemgval  31903  cvmscbv  32630  cvmsdisj  32642  cvmsss2  32646  satfv1  32735  nepss  33073  tailfb  33850  bj-0int  34532  mblfinlem2  35111  qsdisjALTV  36026  lshpinN  36301  elrfi  39650  fipjust  40279  conrel1d  40379  ntrk0kbimka  40757  clsk3nimkb  40758  isotone2  40767  ntrclskb  40787  ntrclsk3  40788  ntrclsk13  40789  csbresgVD  41616  disjf1  41824  qinioo  42187  fouriersw  42888  nnfoctbdjlem  43109  meadjun  43116  caragenel  43149
 Copyright terms: Public domain W3C validator