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

Theorem ineq2 4164
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 4163 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 4159 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4159 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2802 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cin 3907
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-in 3915
This theorem is referenced by:  ineq12  4165  ineq2i  4167  ineq2d  4170  uneqin  4236  intprgOLD  4943  wefrc  5624  onfr  6352  onnseq  8257  qsdisj  8666  disjenex  9012  fiint  9201  elfiun  9299  dffi3  9300  cplem2  9759  dfac5  9997  kmlem2  10020  kmlem13  10031  kmlem14  10032  ackbij1lem16  10104  fin23lem12  10200  fin23lem19  10205  fin23lem33  10214  uzin2  15163  pgpfac1lem3  19785  pgpfac1lem5  19787  pgpfac1  19788  inopn  22170  basis1  22222  basis2  22223  baspartn  22226  fctop  22276  cctop  22278  ordtbaslem  22461  hausnei2  22626  cnhaus  22627  nrmsep  22630  isnrm2  22631  dishaus  22655  ordthauslem  22656  dfconn2  22692  nconnsubb  22696  finlocfin  22793  dissnlocfin  22802  locfindis  22803  kgeni  22810  pthaus  22911  txhaus  22920  xkohaus  22926  regr1lem  23012  fbasssin  23109  fbun  23113  fbunfip  23142  filconn  23156  isufil2  23181  ufileu  23192  filufint  23193  fmfnfmlem4  23230  fmfnfm  23231  fclsopni  23288  fclsbas  23294  fclsrest  23297  isfcf  23307  tsmsfbas  23401  ustincl  23481  ust0  23493  metreslem  23637  methaus  23798  qtopbaslem  24044  metnrmlem3  24146  ismbl  24812  shincl  30121  chincl  30239  chdmm1  30265  ledi  30280  cmbr  30324  cmbr3i  30340  cmbr3  30348  pjoml2  30351  stcltrlem1  31016  mdbr  31034  dmdbr  31039  cvmd  31076  cvexch  31114  sumdmdii  31155  mddmdin0i  31171  ofpreima2  31379  crefeq  32199  ldgenpisyslem1  32535  ldgenpisys  32538  inelsros  32550  diffiunisros  32551  elcarsg  32678  carsgclctunlem2  32692  carsgclctun  32694  ballotlemfval  32862  ballotlemgval  32896  cvmscbv  33625  cvmsdisj  33637  cvmsss2  33641  satfv1  33730  nepss  34064  tailfb  34744  bj-0int  35467  mblfinlem2  36011  qsdisjALTV  36972  lshpinN  37346  elrfi  40882  fipjust  41599  conrel1d  41697  ntrk0kbimka  42075  clsk3nimkb  42076  isotone2  42085  ntrclskb  42105  ntrclsk3  42106  ntrclsk13  42107  csbresgVD  42941  disjf1  43158  qinioo  43526  fouriersw  44225  nnfoctbdjlem  44449  meadjun  44456  caragenel  44489  sepnsepolem2  46704  sepfsepc  46709  iscnrm3rlem8  46729  iscnrm3llem2  46732
  Copyright terms: Public domain W3C validator