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

Theorem ineq1d 3774
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ineq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem ineq1d
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineq1 3768 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 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:  diftpsn3OLD  4273  iinrab2  4513  disji2  4563  disjprg  4572  disjxun  4575  riinint  5290  fnresdisj  5901  fnimadisj  5911  fninfp  6323  ecinxp  7686  fiint  8099  fival  8178  marypha1lem  8199  kmlem12  8843  fin23lem12  9013  fin23lem30  9024  fin23lem33  9027  ttukeylem1  9191  fpwwe2cbv  9308  fpwwe2lem2  9310  fpwwe2  9321  fzval2  12155  fvinim0ffz  12404  limsupval  13999  limsupgval  14001  ello1  14040  elo1  14051  fsum1p  14272  incexclem  14353  fprod1p  14483  smuval2  14988  smueqlem  14996  smumul  14999  setsdm  15670  isacs2  16083  acsfiel  16084  isacs1i  16087  catcval  16515  resscatc  16524  acsficl  16940  lsmdisj3  17865  lsmdisj3a  17871  dprdres  18196  dprdz  18198  dpjdisj  18221  lspdisj2  18894  indistopon  20557  restopnb  20731  ordtrest2  20760  isnrm  20891  cmpcov  20944  cmpsublem  20954  cmpsub  20955  tgcmp  20956  uncmp  20958  hauscmplem  20961  nconsubb  20978  isnlly  21024  dissnlocfin  21084  kgeni  21092  kgencn3  21113  ptcld  21168  ptcnplem  21176  alexsublem  21600  alexsubb  21602  alexsubALTlem2  21604  alexsubALTlem4  21606  alexsubALT  21607  tmdgsum2  21652  tsmsval2  21685  ustexsym  21771  metrest  22080  qtopbaslem  22304  cnheibor  22493  bndth  22496  lebnumii  22504  iscph  22702  csscld  22774  clsocv  22775  ovolicc2  23014  voliunlem3  23044  ioombl  23057  uniioombllem2  23074  uniioombllem4  23077  uniioombllem6  23079  mbflimsup  23156  taylfval  23834  chtval  24553  ppival  24570  ppival2  24571  ppival2g  24572  chtfl  24592  ppiprm  24594  chtprm  24596  chtnprm  24597  chtdif  24601  ppidif  24606  prmorcht  24621  2pthlem2  25892  frgrancvvdeqlem4  26326  chdmj2  27579  cmcmlem  27640  pjoml2  27660  fh2  27668  mdbr  28343  mdi  28344  mdbr3  28346  mdbr4  28347  dmdmd  28349  dmdbr3  28354  dmdbr4  28355  dmdi4  28356  dmdbr5  28357  mddmd2  28358  mdsl1i  28370  cvmdi  28373  mdslmd1lem1  28374  mdslmd1lem2  28375  mdslmd1lem3  28376  mdslmd1lem4  28377  mdslmd1i  28378  mdslmd3i  28381  csmdsymi  28383  mdexchi  28384  atomli  28431  atabsi  28450  sumdmdlem2  28468  dmdbr5ati  28471  difuncomp  28558  disji2f  28578  disjif2  28582  disjxpin  28589  disjunsn  28595  fnresin  28618  locfinreflem  29041  iscref  29045  ordtrest2NEW  29103  ordtconlem1  29104  carsgclctunlem1  29512  totprobd  29621  probmeasb  29625  ballotlemfval  29684  ballotlemfp1  29686  ballotlemgun  29719  bnj1385  29963  bnj1326  30154  iccllyscon  30292  mvrsval  30462  mrsubvrs  30479  mpstval  30492  msubvrs  30517  neibastop2lem  31331  neibastop2  31332  neibastop3  31333  limsucncmpi  31420  ptrest  32374  mblfinlem2  32413  sstotbnd2  32539  cntotbnd  32561  heibor  32586  l1cvat  33156  pmodlem2  33947  pmod2iN  33949  hlmod1i  33956  osumcllem3N  34058  osumcllem9N  34064  pexmidlem6N  34075  pl42lem1N  34079  istrnN  34258  djavalN  35238  dihmeetlem9N  35418  dihmeetlem11N  35420  dihmeetlem12N  35421  dihoml4  35480  djhval  35501  dochexmidlem6  35568  lclkrlem2b  35611  lcfrlem20  35665  lcfrlem23  35668  elrfi  36071  isnacs  36081  mrefg2  36084  mapfzcons2  36096  coeq0i  36130  eldioph2lem2  36138  aomclem8  36445  kelac1  36447  islmodfg  36453  lnr2i  36501  fgraphopab  36603  ntrkbimka  37152  ntrk0kbimka  37153  isotone2  37163  ntrclskb  37183  ntrclsk3  37184  ntrclsk13  37185  neicvgbex  37226  disjrnmpt2  38166  disjinfi  38171  fsumiunss  38439  lptre2pt  38504  stoweidlem50  38740  stoweidlem57  38747  subsaliuncllem  39048  sge0val  39056  sge0iunmptlemre  39105  nnfoctbdjlem  39145  iundjiun  39150  vonvolmbllem  39347  frgrncvvdeqlem4  41467  elbigo  42138  aacllem  42312
  Copyright terms: Public domain W3C validator