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

Theorem ineq2d 3847
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 3841 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614
This theorem is referenced by:  disjpr2OLD  4281  rint0  4549  riin0  4626  disji2  4668  disjprg  4680  disjxun  4683  xpriindi  5291  riinint  5414  reseq2  5423  resindm  5479  predep  5744  onfr  5801  fimacnvinrn  6388  fimacnvinrn2  6389  isofrlem  6630  isoselem  6631  oev2  7648  domss2  8160  funsnfsupp  8340  kmlem11  9020  fpwwe2cbv  9490  fpwwe2lem3  9493  fpwwe2lem8  9497  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  fz1isolem  13283  limsupgle  14252  fsumm1  14524  incexclem  14612  bitsinv1  15211  bitsinvp1  15218  sadcadd  15227  sadadd2  15229  smumullem  15261  ressbas  15977  ressress  15985  restval  16134  ismred2  16310  resscatc  16802  cnvps  17259  cntziinsn  17813  lsmdisj3r  18145  lsmdisj3b  18149  gsummptfzsplitl  18379  dmdprd  18443  subgdmdprd  18479  pgpfaclem1  18526  subrgpropd  18862  crng2idl  19287  obselocv  20120  basis1  20802  baspartn  20806  eltg  20809  tgdom  20830  indistopon  20853  ntrval  20888  clslp  21000  resttopon2  21020  restopnb  21027  paste  21146  nrmsep3  21207  imacmp  21248  cmpsub  21251  bwth  21261  llyi  21325  nllyi  21326  cldllycmp  21346  kgencmp2  21397  ptbasfi  21432  kqdisj  21583  kqcldsat  21584  trfbas2  21694  filss  21704  elfg  21722  flimclslem  21835  fcfneii  21888  tsmsfbas  21978  restutopopn  22089  ressxms  22377  restmetu  22422  qtopbaslem  22609  pi1addf  22893  pi1addval  22894  shftmbl  23352  voliunlem1  23364  voliunlem2  23365  uniioombllem2  23397  uniioombllem4  23400  uniioombllem6  23402  volsup2  23419  volcn  23420  volivth  23421  itg1climres  23526  limciun  23703  dvres3a  23723  ig1pval  23977  p1evtxdeqlem  26464  pthdlem2  26720  eupthp1  27194  omlsi  28391  pjoml  28423  chdmj3  28518  chdmj4  28519  ledi  28527  cmbr  28571  cmbr3  28595  pjoml3  28599  fh1  28605  fh2  28606  dmdbr  29286  dmdmd  29287  dmdbr5  29295  dmdsl3  29302  chirredlem2  29378  chirredlem3  29379  dmdbr6ati  29410  disji2f  29516  disjif2  29520  disjxpin  29527  disjunsn  29533  prsss  30090  carsgclctunlem1  30507  carsgclctunlem2  30509  carsgclctunlem3  30510  ballotlemfval  30679  signsplypnf  30755  ftc2re  30804  fsum2dsub  30813  bnj1326  31220  mvrsval  31528  msrfval  31560  mthmpps  31605  dfpo2  31771  elima4  31803  topbnd  32444  opnbnd  32445  cldbnd  32446  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  neibastop3  32482  neifg  32491  bj-ismoored  33187  bj-diagval  33220  csbpredg  33302  poimirlem3  33542  mblfinlem2  33577  ftc1anclem6  33620  heiborlem3  33742  xrneq2  34282  elrefrels2  34407  refreleq  34410  elcnvrefrels2  34420  pmodN  35454  polvalN  35509  polatN  35535  trnsetN  35761  djavalN  36741  dihmeetbclemN  36910  dihmeetlem11N  36923  djhval  37004  lclkrlem2e  37117  lcfrlem23  37171  lcdlss2N  37226  elrfi  37574  elrfirn  37575  elrfirn2  37576  eldioph2lem1  37640  conrel2d  38273  ntrkbimka  38653  ntrk0kbimka  38654  isotone2  38664  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  clsneibex  38717  neicvgbex  38727  csbresgOLD  39370  inabs3  39538  disjiun2  39540  fresin2  39666  lptioo2  40181  lptioo1  40182  limsupvaluz  40258  cncfuni  40417  fourierdlem48  40689  fourierdlem49  40690  fourierdlem93  40734  qndenserrnbllem  40832  nnfoctbdjlem  40990  carageniuncllem1  41056  carageniuncllem2  41057  hoiqssbllem3  41159  smflimlem3  41302  smflim  41306
  Copyright terms: Public domain W3C validator