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

Theorem ineq1d 4169
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 4163 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cin 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-in 3915
This theorem is referenced by:  iinrab2  5028  disji2  5085  disjprgw  5098  disjprg  5099  disjxun  5101  riinint  5919  fnresdisj  6616  fnimadisj  6628  fninfp  7114  ecinxp  8664  fiint  9201  fival  9281  marypha1lem  9302  kmlem12  10030  fin23lem12  10200  fin23lem30  10211  fin23lem33  10214  ttukeylem1  10378  fpwwe2cbv  10499  fpwwe2lem2  10501  fpwwe2  10512  fzval2  13355  fvinim0ffz  13619  limsupval  15290  limsupgval  15292  ello1  15331  elo1  15342  fsum1p  15572  incexclem  15655  fprod1p  15785  smuval2  16296  smueqlem  16304  smumul  16307  setsdm  16976  isacs2  17467  acsfiel  17468  isacs1i  17471  cat1lem  17916  catcval  17920  resscatc  17929  acsficl  18370  lsmdisj3  19394  lsmdisj3a  19400  dprdres  19736  dprdz  19738  dpjdisj  19761  lspdisj2  20511  indistopon  22273  restopnb  22448  ordtrest2  22477  isnrm  22608  cmpcov  22662  cmpsublem  22672  cmpsub  22673  tgcmp  22674  uncmp  22676  hauscmplem  22679  nconnsubb  22696  isnlly  22742  dissnlocfin  22802  kgeni  22810  kgencn3  22831  ptcld  22886  ptcnplem  22894  alexsublem  23317  alexsubb  23319  alexsubALTlem2  23321  alexsubALTlem4  23323  alexsubALT  23324  tmdgsum2  23369  tsmsval2  23403  ustexsym  23489  metrest  23802  qtopbaslem  24044  cnheibor  24240  bndth  24243  lebnumii  24251  iscph  24456  csscld  24535  clsocv  24536  cphsscph  24537  ovolicc2  24808  voliunlem3  24838  ioombl  24851  uniioombllem2  24869  uniioombllem4  24872  uniioombllem6  24874  mbflimsup  24952  taylfval  25640  chtval  26381  ppival  26398  ppival2  26399  ppival2g  26400  chtfl  26420  ppiprm  26422  chtprm  26424  chtnprm  26425  chtdif  26429  ppidif  26434  prmorcht  26449  nosupbnd2lem1  26985  chdmj2  30270  cmcmlem  30331  pjoml2  30351  fh2  30359  mdbr  31034  mdi  31035  mdbr3  31037  mdbr4  31038  dmdmd  31040  dmdbr3  31045  dmdbr4  31046  dmdi4  31047  dmdbr5  31048  mddmd2  31049  mdsl1i  31061  cvmdi  31064  mdslmd1lem1  31065  mdslmd1lem2  31066  mdslmd1lem3  31067  mdslmd1lem4  31068  mdslmd1i  31069  mdslmd3i  31072  csmdsymi  31074  mdexchi  31075  atomli  31122  atabsi  31141  sumdmdlem2  31159  dmdbr5ati  31162  difuncomp  31269  disji2f  31292  disjif2  31296  disjxpin  31303  disjunsn  31309  fnresin  31337  cycpmco2f1  31767  cycpmconjslem2  31798  locfinreflem  32194  iscref  32198  ordtrest2NEW  32277  ordtconnlem1  32278  carsgclctunlem1  32690  totprobd  32799  probmeasb  32803  ballotlemfval  32862  ballotlemfp1  32864  ballotlemgun  32897  chtvalz  33015  bnj1385  33217  bnj1326  33411  iccllysconn  33617  satfv1  33730  mvrsval  33872  mrsubvrs  33889  mpstval  33902  msubvrs  33927  neibastop2lem  34727  neibastop2  34728  neibastop3  34729  limsucncmpi  34812  bj-ismoore  35471  fvineqsnf1  35776  pibt2  35783  ptrest  35972  mblfinlem2  36011  sstotbnd2  36128  cntotbnd  36150  heibor  36175  xrneq1  36734  disjressuc2  36745  l1cvat  37412  pmodlem2  38205  pmod2iN  38207  hlmod1i  38214  osumcllem3N  38316  osumcllem9N  38322  pexmidlem6N  38333  pl42lem1N  38337  istrnN  38515  djavalN  39493  dihmeetlem9N  39673  dihmeetlem11N  39675  dihmeetlem12N  39676  dihoml4  39735  djhval  39756  dochexmidlem6  39823  lclkrlem2b  39866  lcfrlem20  39920  lcfrlem23  39923  metakunt20  40491  elrfi  40882  isnacs  40892  mrefg2  40895  mapfzcons2  40907  coeq0i  40941  eldioph2lem2  40949  aomclem8  41253  kelac1  41255  islmodfg  41261  lnr2i  41308  fgraphopab  41402  ntrkbimka  42074  ntrk0kbimka  42075  isotone2  42085  ntrclskb  42105  ntrclsk3  42106  ntrclsk13  42107  neicvgbex  42148  disjrnmpt2  43164  disjinfi  43169  uzinico2  43553  uzinico3  43554  fsumiunss  43569  lptre2pt  43634  limsupresre  43690  limsuplesup  43693  limsupresico  43694  limsupvaluz  43702  limsuplt2  43747  liminfval  43753  limsupge  43755  liminfgval  43756  liminfval2  43762  liminfresico  43765  liminflelimsuplem  43769  liminflelimsup  43770  stoweidlem50  44044  stoweidlem57  44051  subsaliuncllem  44351  sge0val  44360  sge0iunmptlemre  44409  nnfoctbdjlem  44449  iundjiun  44454  vonvolmbllem  44654  smfpimcclem  44801  smfsuplem1  44805  f1cof1blem  45057  elbigo  46386  restclsseplem  46696  sepnsepo  46705  aacllem  46993
  Copyright terms: Public domain W3C validator