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

Theorem ineq1d 3775
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 3769 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 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:  diftpsn3OLD  4274  iinrab2  4519  disji2  4569  disjprg  4578  disjxun  4581  riinint  5303  fnresdisj  5915  fnimadisj  5925  fninfp  6345  ecinxp  7709  fiint  8122  fival  8201  marypha1lem  8222  kmlem12  8866  fin23lem12  9036  fin23lem30  9047  fin23lem33  9050  ttukeylem1  9214  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwe2  9344  fzval2  12200  fvinim0ffz  12449  limsupval  14053  limsupgval  14055  ello1  14094  elo1  14105  fsum1p  14326  incexclem  14407  fprod1p  14537  smuval2  15042  smueqlem  15050  smumul  15053  setsdm  15724  isacs2  16137  acsfiel  16138  isacs1i  16141  catcval  16569  resscatc  16578  acsficl  16994  lsmdisj3  17919  lsmdisj3a  17925  dprdres  18250  dprdz  18252  dpjdisj  18275  lspdisj2  18948  indistopon  20615  restopnb  20789  ordtrest2  20818  isnrm  20949  cmpcov  21002  cmpsublem  21012  cmpsub  21013  tgcmp  21014  uncmp  21016  hauscmplem  21019  nconsubb  21036  isnlly  21082  dissnlocfin  21142  kgeni  21150  kgencn3  21171  ptcld  21226  ptcnplem  21234  alexsublem  21658  alexsubb  21660  alexsubALTlem2  21662  alexsubALTlem4  21664  alexsubALT  21665  tmdgsum2  21710  tsmsval2  21743  ustexsym  21829  metrest  22139  qtopbaslem  22372  cnheibor  22562  bndth  22565  lebnumii  22573  iscph  22778  csscld  22856  clsocv  22857  ovolicc2  23097  voliunlem3  23127  ioombl  23140  uniioombllem2  23157  uniioombllem4  23160  uniioombllem6  23162  mbflimsup  23239  taylfval  23917  chtval  24636  ppival  24653  ppival2  24654  ppival2g  24655  chtfl  24675  ppiprm  24677  chtprm  24679  chtnprm  24680  chtdif  24684  ppidif  24689  prmorcht  24704  2pthlem2  26126  frgrancvvdeqlem4  26560  chdmj2  27773  cmcmlem  27834  pjoml2  27854  fh2  27862  mdbr  28537  mdi  28538  mdbr3  28540  mdbr4  28541  dmdmd  28543  dmdbr3  28548  dmdbr4  28549  dmdi4  28550  dmdbr5  28551  mddmd2  28552  mdsl1i  28564  cvmdi  28567  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd1lem3  28570  mdslmd1lem4  28571  mdslmd1i  28572  mdslmd3i  28575  csmdsymi  28577  mdexchi  28578  atomli  28625  atabsi  28644  sumdmdlem2  28662  dmdbr5ati  28665  difuncomp  28752  disji2f  28772  disjif2  28776  disjxpin  28783  disjunsn  28789  fnresin  28812  locfinreflem  29235  iscref  29239  ordtrest2NEW  29297  ordtconlem1  29298  carsgclctunlem1  29706  totprobd  29815  probmeasb  29819  ballotlemfval  29878  ballotlemfp1  29880  ballotlemgun  29913  bnj1385  30157  bnj1326  30348  iccllyscon  30486  mvrsval  30656  mrsubvrs  30673  mpstval  30686  msubvrs  30711  neibastop2lem  31525  neibastop2  31526  neibastop3  31527  limsucncmpi  31614  ptrest  32578  mblfinlem2  32617  sstotbnd2  32743  cntotbnd  32765  heibor  32790  l1cvat  33360  pmodlem2  34151  pmod2iN  34153  hlmod1i  34160  osumcllem3N  34262  osumcllem9N  34268  pexmidlem6N  34279  pl42lem1N  34283  istrnN  34462  djavalN  35442  dihmeetlem9N  35622  dihmeetlem11N  35624  dihmeetlem12N  35625  dihoml4  35684  djhval  35705  dochexmidlem6  35772  lclkrlem2b  35815  lcfrlem20  35869  lcfrlem23  35872  elrfi  36275  isnacs  36285  mrefg2  36288  mapfzcons2  36300  coeq0i  36334  eldioph2lem2  36342  aomclem8  36649  kelac1  36651  islmodfg  36657  lnr2i  36705  fgraphopab  36807  ntrkbimka  37356  ntrk0kbimka  37357  isotone2  37367  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  neicvgbex  37430  disjrnmpt2  38370  disjinfi  38375  fsumiunss  38642  lptre2pt  38707  stoweidlem50  38943  stoweidlem57  38950  subsaliuncllem  39251  sge0val  39259  sge0iunmptlemre  39308  nnfoctbdjlem  39348  iundjiun  39353  vonvolmbllem  39550  frgrncvvdeqlem4  41472  elbigo  42143  aacllem  42356
  Copyright terms: Public domain W3C validator