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

Theorem ineq2d 4193
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 4187 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  cin 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1533  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rab 3152  df-in 3947
This theorem is referenced by:  rint0  4914  riin0  5001  disji2  5045  disjprgw  5058  disjprg  5059  disjxun  5061  xpriindi  5706  riinint  5838  reseq2  5847  resindm  5899  predep  6173  onfr  6229  fimacnvinrn  6838  fimacnvinrn2  6839  isofrlem  7087  isoselem  7088  oev2  8144  domss2  8670  funsnfsupp  8851  kmlem11  9580  fpwwe2cbv  10046  fpwwe2lem3  10049  fpwwe2lem8  10053  fpwwe2lem12  10057  fpwwe2lem13  10058  fpwwe2  10059  fz1isolem  13814  limsupgle  14829  fsumm1  15101  incexclem  15186  bitsinv1  15786  bitsinvp1  15793  sadcadd  15802  sadadd2  15804  smumullem  15836  ressbas  16549  ressress  16557  restval  16695  ismred2  16869  resscatc  17360  cnvps  17817  cntziinsn  18410  lsmdisj3r  18748  lsmdisj3b  18752  gsummptfzsplitl  18989  dmdprd  19056  subgdmdprd  19092  pgpfaclem1  19139  subrgpropd  19506  crng2idl  19947  obselocv  20807  basis1  21493  baspartn  21497  eltg  21500  tgdom  21521  indistopon  21544  ntrval  21579  clslp  21691  resttopon2  21711  restopnb  21718  paste  21837  nrmsep3  21898  imacmp  21940  cmpsub  21943  bwth  21953  llyi  22017  nllyi  22018  cldllycmp  22038  kgencmp2  22089  ptbasfi  22124  kqdisj  22275  kqcldsat  22276  trfbas2  22386  filss  22396  elfg  22414  flimclslem  22527  fcfneii  22580  tsmsfbas  22670  restutopopn  22781  ressxms  23069  restmetu  23114  qtopbaslem  23301  pi1addf  23585  pi1addval  23586  shftmbl  24073  voliunlem1  24085  voliunlem2  24086  uniioombllem2  24118  uniioombllem4  24121  uniioombllem6  24123  volsup2  24140  volcn  24141  volivth  24142  itg1climres  24249  limciun  24426  dvres3a  24446  ig1pval  24700  p1evtxdeqlem  27227  pthdlem2  27482  eupthp1  27928  omlsi  29114  pjoml  29146  chdmj3  29241  chdmj4  29242  ledi  29250  cmbr  29294  cmbr3  29318  pjoml3  29322  fh1  29328  fh2  29329  dmdbr  30009  dmdmd  30010  dmdbr5  30018  dmdsl3  30025  chirredlem2  30101  chirredlem3  30102  dmdbr6ati  30133  unidifsnne  30229  disji2f  30261  disjif2  30265  disjxpin  30272  disjunsn  30278  cycpmco2f1  30699  tocyccntz  30719  dimkerim  30928  prsss  31064  carsgclctunlem1  31480  carsgclctunlem2  31482  carsgclctunlem3  31483  ballotlemfval  31652  signsplypnf  31725  ftc2re  31774  fsum2dsub  31783  bnj1326  32201  f1resfz0f1d  32264  pthhashvtx  32277  satfv1  32513  satefv  32564  mvrsval  32655  msrfval  32687  mthmpps  32732  dfpo2  32894  elima4  32922  topbnd  33575  opnbnd  33576  cldbnd  33577  neibastop1  33610  neibastop2lem  33611  neibastop2  33612  neibastop3  33613  neifg  33622  bj-ismoored  34299  csbpredg  34495  pibt2  34586  poimirlem3  34781  mblfinlem2  34816  ftc1anclem6  34858  heiborlem3  34978  xrneq2  35518  elrefrels2  35643  refreleq  35646  elcnvrefrels2  35656  pmodN  36872  polvalN  36927  polatN  36953  trnsetN  37178  djavalN  38157  dihmeetbclemN  38326  dihmeetlem11N  38339  djhval  38420  lclkrlem2e  38533  lcfrlem23  38587  lcdlss2N  38642  elrfi  39175  elrfirn  39176  elrfirn2  39177  eldioph2lem1  39241  conrel2d  39893  ntrkbimka  40272  ntrk0kbimka  40273  isotone2  40283  ntrclskb  40303  ntrclsk3  40304  ntrclsk13  40305  clsneibex  40336  neicvgbex  40346  inabs3  41202  disjiun2  41204  fresin2  41312  lptioo2  41796  lptioo1  41797  limsupvaluz  41873  cncfuni  42053  fourierdlem48  42324  fourierdlem49  42325  fourierdlem93  42369  qndenserrnbllem  42464  nnfoctbdjlem  42622  carageniuncllem1  42688  carageniuncllem2  42689  hoiqssbllem3  42791  smflimlem3  42934  smflim  42938
  Copyright terms: Public domain W3C validator