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

Theorem ineq2 4165
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 4164 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 4160 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4160 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2803 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cin 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-in 3916
This theorem is referenced by:  ineq12  4166  ineq2i  4168  ineq2d  4171  uneqin  4237  intprgOLD  4944  wefrc  5625  onfr  6353  onnseq  8258  qsdisj  8667  disjenex  9013  fiint  9202  elfiun  9300  dffi3  9301  cplem2  9760  dfac5  9998  kmlem2  10021  kmlem13  10032  kmlem14  10033  ackbij1lem16  10105  fin23lem12  10201  fin23lem19  10206  fin23lem33  10215  uzin2  15164  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  30109  chincl  30227  chdmm1  30253  ledi  30268  cmbr  30312  cmbr3i  30328  cmbr3  30336  pjoml2  30339  stcltrlem1  31004  mdbr  31022  dmdbr  31027  cvmd  31064  cvexch  31102  sumdmdii  31143  mddmdin0i  31159  ofpreima2  31367  crefeq  32187  ldgenpisyslem1  32523  ldgenpisys  32526  inelsros  32538  diffiunisros  32539  elcarsg  32666  carsgclctunlem2  32680  carsgclctun  32682  ballotlemfval  32850  ballotlemgval  32884  cvmscbv  33613  cvmsdisj  33625  cvmsss2  33629  satfv1  33718  nepss  34052  tailfb  34735  bj-0int  35458  mblfinlem2  36002  qsdisjALTV  36963  lshpinN  37337  elrfi  40851  fipjust  41568  conrel1d  41666  ntrk0kbimka  42044  clsk3nimkb  42045  isotone2  42054  ntrclskb  42074  ntrclsk3  42075  ntrclsk13  42076  csbresgVD  42910  disjf1  43121  qinioo  43483  fouriersw  44182  nnfoctbdjlem  44404  meadjun  44411  caragenel  44444  sepnsepolem2  46655  sepfsepc  46660  iscnrm3rlem8  46680  iscnrm3llem2  46683
  Copyright terms: Public domain W3C validator