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

Theorem ineq2 4182
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 4180 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 4177 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4177 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2881 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cin 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942
This theorem is referenced by:  ineq12  4183  ineq2i  4185  ineq2d  4188  uneqin  4254  intprg  4903  wefrc  5543  onfr  6224  onnseq  7972  qsdisj  8364  disjenex  8664  fiint  8784  elfiun  8883  dffi3  8884  cplem2  9308  dfac5  9543  kmlem2  9566  kmlem13  9577  kmlem14  9578  ackbij1lem16  9646  fin23lem12  9742  fin23lem19  9747  fin23lem33  9756  uzin2  14694  pgpfac1lem3  19130  pgpfac1lem5  19132  pgpfac1  19133  inopn  21437  basis1  21488  basis2  21489  baspartn  21492  fctop  21542  cctop  21544  ordtbaslem  21726  hausnei2  21891  cnhaus  21892  nrmsep  21895  isnrm2  21896  dishaus  21920  ordthauslem  21921  dfconn2  21957  nconnsubb  21961  finlocfin  22058  dissnlocfin  22067  locfindis  22068  kgeni  22075  pthaus  22176  txhaus  22185  xkohaus  22191  regr1lem  22277  fbasssin  22374  fbun  22378  fbunfip  22407  filconn  22421  isufil2  22446  ufileu  22457  filufint  22458  fmfnfmlem4  22495  fmfnfm  22496  fclsopni  22553  fclsbas  22559  fclsrest  22562  isfcf  22572  tsmsfbas  22665  ustincl  22745  ust0  22757  metreslem  22901  methaus  23059  qtopbaslem  23296  metnrmlem3  23398  ismbl  24056  shincl  29086  chincl  29204  chdmm1  29230  ledi  29245  cmbr  29289  cmbr3i  29305  cmbr3  29313  pjoml2  29316  stcltrlem1  29981  mdbr  29999  dmdbr  30004  cvmd  30041  cvexch  30079  sumdmdii  30120  mddmdin0i  30136  ofpreima2  30340  crefeq  31009  ldgenpisyslem1  31322  ldgenpisys  31325  inelsros  31337  diffiunisros  31338  elcarsg  31463  carsgclctunlem2  31477  carsgclctun  31479  ballotlemfval  31647  ballotlemgval  31681  cvmscbv  32403  cvmsdisj  32415  cvmsss2  32419  satfv1  32508  nepss  32846  tailfb  33623  bj-0int  34288  mblfinlem2  34812  qsdisjALTV  35732  lshpinN  36007  elrfi  39171  fipjust  39804  conrel1d  39888  ntrk0kbimka  40269  clsk3nimkb  40270  isotone2  40279  ntrclskb  40299  ntrclsk3  40300  ntrclsk13  40301  csbresgVD  41109  disjf1  41323  qinioo  41691  fouriersw  42397  nnfoctbdjlem  42618  meadjun  42625  caragenel  42658
  Copyright terms: Public domain W3C validator