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

Theorem ineq2 3770
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 3769 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 3767 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 3767 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2669 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  cin 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547
This theorem is referenced by:  ineq12  3771  ineq2i  3773  ineq2d  3776  uneqin  3837  intprg  4446  wefrc  5032  onfr  5680  onnseq  7328  qsdisj  7711  disjenex  8003  fiint  8122  elfiun  8219  dffi3  8220  cplem2  8636  dfac5  8834  kmlem2  8856  kmlem13  8867  kmlem14  8868  ackbij1lem16  8940  fin23lem12  9036  fin23lem19  9041  fin23lem33  9050  uzin2  13932  pgpfac1lem3  18299  pgpfac1lem5  18301  pgpfac1  18302  inopn  20529  basis1  20565  basis2  20566  baspartn  20569  fctop  20618  cctop  20620  ordtbaslem  20802  hausnei2  20967  cnhaus  20968  nrmsep  20971  isnrm2  20972  dishaus  20996  ordthauslem  20997  dfcon2  21032  nconsubb  21036  finlocfin  21133  dissnlocfin  21142  locfindis  21143  kgeni  21150  pthaus  21251  txhaus  21260  xkohaus  21266  regr1lem  21352  fbasssin  21450  fbun  21454  fbunfip  21483  filcon  21497  isufil2  21522  ufileu  21533  filufint  21534  fmfnfmlem4  21571  fmfnfm  21572  fclsopni  21629  fclsbas  21635  fclsrest  21638  isfcf  21648  tsmsfbas  21741  ustincl  21821  ust0  21833  metreslem  21977  methaus  22135  qtopbaslem  22372  metnrmlem3  22472  ismbl  23101  shincl  27624  chincl  27742  chdmm1  27768  ledi  27783  cmbr  27827  cmbr3i  27843  cmbr3  27851  pjoml2  27854  stcltrlem1  28519  mdbr  28537  dmdbr  28542  cvmd  28579  cvexch  28617  sumdmdii  28658  mddmdin0i  28674  ofpreima2  28849  crefeq  29240  ldgenpisyslem1  29553  ldgenpisys  29556  inelsros  29568  diffiunisros  29569  elcarsg  29694  carsgclctunlem2  29708  carsgclctun  29710  ballotlemfval  29878  ballotlemgval  29912  cvmscbv  30494  cvmsdisj  30506  cvmsss2  30510  nepss  30854  tailfb  31542  mblfinlem2  32617  lshpinN  33294  elrfi  36275  fipjust  36889  conrel1d  36974  ntrk0kbimka  37357  clsk3nimkb  37358  isotone2  37367  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  csbresgVD  38153  disjf1  38364  qinioo  38609  fouriersw  39124  nnfoctbdjlem  39348  meadjun  39355  caragenel  39385
  Copyright terms: Public domain W3C validator