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

Theorem ineq2d 4020
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 4014 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cin 3775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783
This theorem is referenced by:  rint0  4716  riin0  4793  disji2  4835  disjprg  4847  disjxun  4849  xpriindi  5467  riinint  5590  reseq2  5599  resindm  5656  predep  5926  onfr  5982  fimacnvinrn  6573  fimacnvinrn2  6574  isofrlem  6817  isoselem  6818  oev2  7843  domss2  8361  funsnfsupp  8541  kmlem11  9270  fpwwe2cbv  9740  fpwwe2lem3  9743  fpwwe2lem8  9747  fpwwe2lem12  9751  fpwwe2lem13  9752  fpwwe2  9753  fz1isolem  13465  limsupgle  14434  fsumm1  14706  incexclem  14793  bitsinv1  15386  bitsinvp1  15393  sadcadd  15402  sadadd2  15404  smumullem  15436  ressbas  16144  ressress  16153  restval  16295  ismred2  16471  resscatc  16962  cnvps  17420  cntziinsn  17971  lsmdisj3r  18303  lsmdisj3b  18307  gsummptfzsplitl  18537  dmdprd  18602  subgdmdprd  18638  pgpfaclem1  18685  subrgpropd  19021  crng2idl  19451  obselocv  20286  basis1  20972  baspartn  20976  eltg  20979  tgdom  21000  indistopon  21023  ntrval  21058  clslp  21170  resttopon2  21190  restopnb  21197  paste  21316  nrmsep3  21377  imacmp  21418  cmpsub  21421  bwth  21431  llyi  21495  nllyi  21496  cldllycmp  21516  kgencmp2  21567  ptbasfi  21602  kqdisj  21753  kqcldsat  21754  trfbas2  21864  filss  21874  elfg  21892  flimclslem  22005  fcfneii  22058  tsmsfbas  22148  restutopopn  22259  ressxms  22547  restmetu  22592  qtopbaslem  22779  pi1addf  23063  pi1addval  23064  shftmbl  23525  voliunlem1  23537  voliunlem2  23538  uniioombllem2  23570  uniioombllem4  23573  uniioombllem6  23575  volsup2  23592  volcn  23593  volivth  23594  itg1climres  23701  limciun  23878  dvres3a  23898  ig1pval  24152  p1evtxdeqlem  26642  pthdlem2  26898  eupthp1  27395  omlsi  28597  pjoml  28629  chdmj3  28724  chdmj4  28725  ledi  28733  cmbr  28777  cmbr3  28801  pjoml3  28805  fh1  28811  fh2  28812  dmdbr  29492  dmdmd  29493  dmdbr5  29501  dmdsl3  29508  chirredlem2  29584  chirredlem3  29585  dmdbr6ati  29616  disji2f  29721  disjif2  29725  disjxpin  29732  disjunsn  29738  prsss  30293  carsgclctunlem1  30710  carsgclctunlem2  30712  carsgclctunlem3  30713  ballotlemfval  30882  signsplypnf  30958  ftc2re  31007  fsum2dsub  31016  bnj1326  31422  mvrsval  31730  msrfval  31762  mthmpps  31807  dfpo2  31972  elima4  32004  topbnd  32645  opnbnd  32646  cldbnd  32647  neibastop1  32680  neibastop2lem  32681  neibastop2  32682  neibastop3  32683  neifg  32692  bj-ismoored  33375  bj-diagval  33409  csbpredg  33491  poimirlem3  33727  mblfinlem2  33762  ftc1anclem6  33804  heiborlem3  33925  xrneq2  34457  elrefrels2  34582  refreleq  34585  elcnvrefrels2  34595  pmodN  35632  polvalN  35687  polatN  35713  trnsetN  35938  djavalN  36917  dihmeetbclemN  37086  dihmeetlem11N  37099  djhval  37180  lclkrlem2e  37293  lcfrlem23  37347  lcdlss2N  37402  elrfi  37760  elrfirn  37761  elrfirn2  37762  eldioph2lem1  37826  conrel2d  38457  ntrkbimka  38837  ntrk0kbimka  38838  isotone2  38848  ntrclskb  38868  ntrclsk3  38869  ntrclsk13  38870  clsneibex  38901  neicvgbex  38911  csbresgOLD  39551  inabs3  39718  disjiun2  39720  fresin2  39842  lptioo2  40344  lptioo1  40345  limsupvaluz  40421  cncfuni  40580  fourierdlem48  40851  fourierdlem49  40852  fourierdlem93  40896  qndenserrnbllem  40994  nnfoctbdjlem  41152  carageniuncllem1  41218  carageniuncllem2  41219  hoiqssbllem3  41321  smflimlem3  41464  smflim  41468
  Copyright terms: Public domain W3C validator