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

Theorem ineq2d 3775
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 3769 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cin 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546
This theorem is referenced by:  disjpr2OLD  4194  rint0  4446  riin0  4524  disji2  4563  disjprg  4572  disjxun  4575  xpriindi  5167  riinint  5289  reseq2  5298  resindm  5350  predep  5608  onfr  5665  fimacnvinrn  6240  fimacnvinrn2  6241  isofrlem  6467  isoselem  6468  oev2  7467  domss2  7981  funsnfsupp  8159  kmlem11  8842  fpwwe2cbv  9308  fpwwe2lem3  9311  fpwwe2lem8  9315  fpwwe2lem12  9319  fpwwe2lem13  9320  fpwwe2  9321  fz1isolem  13056  limsupgle  14004  fsumm1  14272  incexclem  14355  bitsinv1  14950  bitsinvp1  14957  sadcadd  14966  sadadd2  14968  smumullem  15000  ressbas  15705  ressress  15713  restval  15858  ismred2  16034  resscatc  16526  cnvps  16983  cntziinsn  17538  lsmdisj3r  17870  lsmdisj3b  17874  gsummptfzsplitl  18104  dmdprd  18168  subgdmdprd  18204  pgpfaclem1  18251  subrgpropd  18585  crng2idl  19008  obselocv  19838  basis1  20512  baspartn  20516  eltg  20519  tgdom  20540  indistopon  20562  ntrval  20597  clslp  20709  resttopon2  20729  restopnb  20736  paste  20855  nrmsep3  20916  imacmp  20957  cmpsub  20960  bwth  20970  llyi  21034  nllyi  21035  cldllycmp  21055  kgencmp2  21106  ptbasfi  21141  kqdisj  21292  kqcldsat  21293  trfbas2  21404  filss  21414  elfg  21432  flimclslem  21545  fcfneii  21598  tsmsfbas  21688  restutopopn  21799  ressxms  22087  restmetu  22132  qtopbaslem  22319  pi1addf  22602  pi1addval  22603  shftmbl  23057  voliunlem1  23069  voliunlem2  23070  uniioombllem2  23101  uniioombllem4  23104  uniioombllem6  23106  volsup2  23123  volcn  23124  volivth  23125  itg1climres  23231  limciun  23408  dvres3a  23428  ig1pval  23680  2pthlem2  25919  frgrancvvdeqlem4  26353  omlsi  27440  pjoml  27472  chdmj3  27567  chdmj4  27568  ledi  27576  cmbr  27620  cmbr3  27644  pjoml3  27648  fh1  27654  fh2  27655  dmdbr  28335  dmdmd  28336  dmdbr5  28344  dmdsl3  28351  chirredlem2  28427  chirredlem3  28428  dmdbr6ati  28459  disji2f  28565  disjif2  28569  disjxpin  28576  disjunsn  28582  prsss  29083  carsgclctunlem1  29499  carsgclctunlem2  29501  carsgclctunlem3  29502  ballotlemfval  29671  signsplypnf  29746  bnj1326  30141  mvrsval  30449  msrfval  30481  mthmpps  30526  dfpo2  30691  elima4  30717  topbnd  31282  opnbnd  31283  cldbnd  31284  neibastop1  31317  neibastop2lem  31318  neibastop2  31319  neibastop3  31320  neifg  31329  bj-diagval  32050  csbpredg  32131  poimirlem3  32365  mblfinlem2  32400  ftc1anclem6  32443  heiborlem3  32565  pmodN  33937  polvalN  33992  polatN  34018  trnsetN  34244  djavalN  35225  dihmeetbclemN  35394  dihmeetlem11N  35407  djhval  35488  lclkrlem2e  35601  lcfrlem23  35655  lcdlss2N  35710  elrfi  36058  elrfirn  36059  elrfirn2  36060  eldioph2lem1  36124  conrel2d  36758  ntrkbimka  37139  ntrk0kbimka  37140  isotone2  37150  ntrclskb  37170  ntrclsk3  37171  ntrclsk13  37172  clsneibex  37203  neicvgbex  37213  csbresgOLD  37860  inabs3  38032  disjiun2  38034  fresin2  38130  lptioo2  38481  lptioo1  38482  cncfuni  38555  fourierdlem48  38830  fourierdlem49  38831  fourierdlem93  38875  qndenserrnbllem  38973  nnfoctbdjlem  39131  carageniuncllem1  39194  carageniuncllem2  39195  hoiqssbllem3  39297  smflimlem3  39442  smflim  39446  resisresindm  40114  p1evtxdeqlem  40709  pthdlem2  40955  eupthp1  41365  frgrncvvdeqlem4  41453
  Copyright terms: Public domain W3C validator