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

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

Proof of Theorem ineq2d
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineq2 4180 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-in 3940
This theorem is referenced by:  rint0  4907  riin0  4995  disji2  5039  disjprgw  5052  disjprg  5053  disjxun  5055  xpriindi  5700  riinint  5832  reseq2  5841  resindm  5893  predep  6167  onfr  6223  fimacnvinrn  6832  fimacnvinrn2  6833  isofrlem  7082  isoselem  7083  oev2  8137  domss2  8664  funsnfsupp  8845  kmlem11  9574  fpwwe2cbv  10040  fpwwe2lem3  10043  fpwwe2lem8  10047  fpwwe2lem12  10051  fpwwe2lem13  10052  fpwwe2  10053  fz1isolem  13807  limsupgle  14822  fsumm1  15094  incexclem  15179  bitsinv1  15779  bitsinvp1  15786  sadcadd  15795  sadadd2  15797  smumullem  15829  ressbas  16542  ressress  16550  restval  16688  ismred2  16862  resscatc  17353  cnvps  17810  cntziinsn  18403  lsmdisj3r  18741  lsmdisj3b  18745  gsummptfzsplitl  18982  dmdprd  19049  subgdmdprd  19085  pgpfaclem1  19132  subrgpropd  19499  crng2idl  19940  obselocv  20800  basis1  21486  baspartn  21490  eltg  21493  tgdom  21514  indistopon  21537  ntrval  21572  clslp  21684  resttopon2  21704  restopnb  21711  paste  21830  nrmsep3  21891  imacmp  21933  cmpsub  21936  bwth  21946  llyi  22010  nllyi  22011  cldllycmp  22031  kgencmp2  22082  ptbasfi  22117  kqdisj  22268  kqcldsat  22269  trfbas2  22379  filss  22389  elfg  22407  flimclslem  22520  fcfneii  22573  tsmsfbas  22663  restutopopn  22774  ressxms  23062  restmetu  23107  qtopbaslem  23294  pi1addf  23578  pi1addval  23579  shftmbl  24066  voliunlem1  24078  voliunlem2  24079  uniioombllem2  24111  uniioombllem4  24114  uniioombllem6  24116  volsup2  24133  volcn  24134  volivth  24135  itg1climres  24242  limciun  24419  dvres3a  24439  ig1pval  24693  p1evtxdeqlem  27221  pthdlem2  27476  eupthp1  27922  omlsi  29108  pjoml  29140  chdmj3  29235  chdmj4  29236  ledi  29244  cmbr  29288  cmbr3  29312  pjoml3  29316  fh1  29322  fh2  29323  dmdbr  30003  dmdmd  30004  dmdbr5  30012  dmdsl3  30019  chirredlem2  30095  chirredlem3  30096  dmdbr6ati  30127  unidifsnne  30223  disji2f  30255  disjif2  30259  disjxpin  30266  disjunsn  30272  cycpmco2f1  30693  tocyccntz  30713  dimkerim  30922  prsss  31058  carsgclctunlem1  31474  carsgclctunlem2  31476  carsgclctunlem3  31477  ballotlemfval  31646  signsplypnf  31719  ftc2re  31768  fsum2dsub  31777  bnj1326  32195  f1resfz0f1d  32258  pthhashvtx  32271  satfv1  32507  satefv  32558  mvrsval  32649  msrfval  32681  mthmpps  32726  dfpo2  32888  elima4  32916  topbnd  33569  opnbnd  33570  cldbnd  33571  neibastop1  33604  neibastop2lem  33605  neibastop2  33606  neibastop3  33607  neifg  33616  bj-ismoored  34293  csbpredg  34489  pibt2  34580  poimirlem3  34776  mblfinlem2  34811  ftc1anclem6  34853  heiborlem3  34972  xrneq2  35512  elrefrels2  35637  refreleq  35640  elcnvrefrels2  35650  pmodN  36866  polvalN  36921  polatN  36947  trnsetN  37172  djavalN  38151  dihmeetbclemN  38320  dihmeetlem11N  38333  djhval  38414  lclkrlem2e  38527  lcfrlem23  38581  lcdlss2N  38636  elrfi  39169  elrfirn  39170  elrfirn2  39171  eldioph2lem1  39235  conrel2d  39887  ntrkbimka  40266  ntrk0kbimka  40267  isotone2  40277  ntrclskb  40297  ntrclsk3  40298  ntrclsk13  40299  clsneibex  40330  neicvgbex  40340  inabs3  41195  disjiun2  41197  fresin2  41304  lptioo2  41788  lptioo1  41789  limsupvaluz  41865  cncfuni  42045  fourierdlem48  42316  fourierdlem49  42317  fourierdlem93  42361  qndenserrnbllem  42456  nnfoctbdjlem  42614  carageniuncllem1  42680  carageniuncllem2  42681  hoiqssbllem3  42783  smflimlem3  42926  smflim  42930
  Copyright terms: Public domain W3C validator