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

Theorem ineq2 3769
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 3768 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 3766 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 3766 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2668 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cin 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546
This theorem is referenced by:  ineq12  3770  ineq2i  3772  ineq2d  3775  uneqin  3836  intprg  4440  wefrc  5021  onfr  5665  onnseq  7305  qsdisj  7688  disjenex  7980  fiint  8099  elfiun  8196  dffi3  8197  cplem2  8613  dfac5  8811  kmlem2  8833  kmlem13  8844  kmlem14  8845  ackbij1lem16  8917  fin23lem12  9013  fin23lem19  9018  fin23lem33  9027  uzin2  13880  pgpfac1lem3  18247  pgpfac1lem5  18249  pgpfac1  18250  inopn  20476  basis1  20512  basis2  20513  baspartn  20516  fctop  20565  cctop  20567  ordtbaslem  20749  hausnei2  20914  cnhaus  20915  nrmsep  20918  isnrm2  20919  dishaus  20943  ordthauslem  20944  dfcon2  20979  nconsubb  20983  finlocfin  21080  dissnlocfin  21089  locfindis  21090  kgeni  21097  pthaus  21198  txhaus  21207  xkohaus  21213  regr1lem  21299  fbasssin  21397  fbun  21401  fbunfip  21430  filcon  21444  isufil2  21469  ufileu  21480  filufint  21481  fmfnfmlem4  21518  fmfnfm  21519  fclsopni  21576  fclsbas  21582  fclsrest  21585  isfcf  21595  tsmsfbas  21688  ustincl  21768  ust0  21780  metreslem  21924  methaus  22082  qtopbaslem  22319  metnrmlem3  22419  ismbl  23045  shincl  27417  chincl  27535  chdmm1  27561  ledi  27576  cmbr  27620  cmbr3i  27636  cmbr3  27644  pjoml2  27647  stcltrlem1  28312  mdbr  28330  dmdbr  28335  cvmd  28372  cvexch  28410  sumdmdii  28451  mddmdin0i  28467  ofpreima2  28642  crefeq  29033  ldgenpisyslem1  29346  ldgenpisys  29349  inelsros  29361  diffiunisros  29362  elcarsg  29487  carsgclctunlem2  29501  carsgclctun  29503  ballotlemfval  29671  ballotlemgval  29705  cvmscbv  30287  cvmsdisj  30299  cvmsss2  30303  nepss  30647  tailfb  31335  mblfinlem2  32400  lshpinN  33077  elrfi  36058  fipjust  36672  conrel1d  36757  ntrk0kbimka  37140  clsk3nimkb  37141  isotone2  37150  ntrclskb  37170  ntrclsk3  37171  ntrclsk13  37172  csbresgVD  37936  disjf1  38147  qinioo  38392  fouriersw  38907  nnfoctbdjlem  39131  meadjun  39138  caragenel  39168
  Copyright terms: Public domain W3C validator