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

Theorem ineq2 3951
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 3950 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 3948 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 3948 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2819 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722
This theorem is referenced by:  ineq12  3952  ineq2i  3954  ineq2d  3957  uneqin  4021  intprg  4663  wefrc  5260  onfr  5924  onnseq  7611  qsdisj  7993  disjenex  8285  fiint  8404  elfiun  8503  dffi3  8504  cplem2  8928  dfac5  9161  kmlem2  9185  kmlem13  9196  kmlem14  9197  ackbij1lem16  9269  fin23lem12  9365  fin23lem19  9370  fin23lem33  9379  uzin2  14303  pgpfac1lem3  18696  pgpfac1lem5  18698  pgpfac1  18699  inopn  20926  basis1  20976  basis2  20977  baspartn  20980  fctop  21030  cctop  21032  ordtbaslem  21214  hausnei2  21379  cnhaus  21380  nrmsep  21383  isnrm2  21384  dishaus  21408  ordthauslem  21409  dfconn2  21444  nconnsubb  21448  finlocfin  21545  dissnlocfin  21554  locfindis  21555  kgeni  21562  pthaus  21663  txhaus  21672  xkohaus  21678  regr1lem  21764  fbasssin  21861  fbun  21865  fbunfip  21894  filconn  21908  isufil2  21933  ufileu  21944  filufint  21945  fmfnfmlem4  21982  fmfnfm  21983  fclsopni  22040  fclsbas  22046  fclsrest  22049  isfcf  22059  tsmsfbas  22152  ustincl  22232  ust0  22244  metreslem  22388  methaus  22546  qtopbaslem  22783  metnrmlem3  22885  ismbl  23514  shincl  28570  chincl  28688  chdmm1  28714  ledi  28729  cmbr  28773  cmbr3i  28789  cmbr3  28797  pjoml2  28800  stcltrlem1  29465  mdbr  29483  dmdbr  29488  cvmd  29525  cvexch  29563  sumdmdii  29604  mddmdin0i  29620  ofpreima2  29796  crefeq  30242  ldgenpisyslem1  30556  ldgenpisys  30559  inelsros  30571  diffiunisros  30572  elcarsg  30697  carsgclctunlem2  30711  carsgclctun  30713  ballotlemfval  30881  ballotlemgval  30915  cvmscbv  31568  cvmsdisj  31580  cvmsss2  31584  nepss  31927  tailfb  32699  bj-0int  33379  mblfinlem2  33778  lshpinN  34797  elrfi  37777  fipjust  38390  conrel1d  38475  ntrk0kbimka  38857  clsk3nimkb  38858  isotone2  38867  ntrclskb  38887  ntrclsk3  38888  ntrclsk13  38889  csbresgVD  39648  disjf1  39886  qinioo  40283  fouriersw  40969  nnfoctbdjlem  41193  meadjun  41200  caragenel  41233
  Copyright terms: Public domain W3C validator