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

Theorem ineq2d 3700
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
ineq2d  |-  ( ph  ->  ( C  i^i  A
)  =  ( C  i^i  B ) )

Proof of Theorem ineq2d
StepHypRef Expression
1 ineq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ineq2 3694 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C  i^i  A
)  =  ( C  i^i  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    i^i cin 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483
This theorem is referenced by:  disjpr2  4090  rint0  4322  riin0  4399  disji2  4434  disjprg  4443  disjxun  4445  onfr  4917  xpriindi  5139  riinint  5259  reseq2  5268  csbresgOLD  5277  resindm  5318  isofrlem  6224  isoselem  6225  oev2  7173  domss2  7676  funsnfsupp  7853  kmlem11  8540  fpwwe2cbv  9008  fpwwe2lem3  9011  fpwwe2lem8  9015  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  fz1isolem  12476  limsupgle  13263  fsumm1  13529  incexclem  13611  bitsinv1  13951  bitsinvp1  13958  sadcadd  13967  sadadd2  13969  smumullem  14001  ressbas  14545  ressress  14552  restval  14682  ismred2  14858  resscatc  15290  cnvps  15699  cntziinsn  16177  lsmdisj3r  16510  lsmdisj3b  16514  gsummptfzsplitl  16756  dmdprd  16832  subgdmdprd  16883  pgpfaclem1  16934  subrgpropd  17263  crng2idl  17686  obselocv  18554  basis1  19246  baspartn  19250  eltg  19253  tgdom  19274  indistopon  19296  ntrval  19331  clslp  19443  resttopon2  19463  restopnb  19470  paste  19589  nrmsep3  19650  imacmp  19691  cmpsub  19694  bwth  19704  llyi  19769  nllyi  19770  cldllycmp  19790  kgencmp2  19810  ptbasfi  19845  kqdisj  19996  kqcldsat  19997  trfbas2  20107  filss  20117  elfg  20135  flimclslem  20248  fcfneii  20301  tsmsfbas  20389  restutopopn  20504  ressxms  20791  restmetu  20853  qtopbaslem  21028  pi1addf  21310  pi1addval  21311  shftmbl  21712  voliunlem1  21723  voliunlem2  21724  uniioombllem2  21755  uniioombllem4  21758  uniioombllem6  21760  volsup2  21777  volcn  21778  volivth  21779  itg1climres  21884  limciun  22061  dvres3a  22081  ig1pval  22336  2pthlem2  24302  frgrancvvdeqlem4  24738  issubgo  25009  omlsi  26026  pjoml  26058  chdmj3  26153  chdmj4  26154  ledi  26162  cmbr  26206  cmbr3  26230  pjoml3  26234  fh1  26240  fh2  26241  dmdbr  26922  dmdmd  26923  dmdbr5  26931  dmdsl3  26938  chirredlem2  27014  chirredlem3  27015  dmdbr6ati  27046  disji2f  27139  disjif2  27143  disjxpin  27148  disjunsn  27154  fimacnvinrn  27176  fimacnvinrn2  27177  prsss  27562  ordtrestNEW  27567  ballotlemfval  28096  signsplypnf  28175  dfpo2  28789  elima4  28814  predep  28877  mblfinlem2  29657  ftc1anclem6  29700  topbnd  29747  opnbnd  29748  cldbnd  29749  neibastop1  29808  neibastop2lem  29809  neibastop2  29810  neibastop3  29811  neifg  29820  heiborlem3  29940  elrfi  30258  elrfirn  30259  elrfirn2  30260  eldioph2lem1  30325  fresin2  31054  lptioo2  31201  lptioo1  31202  cncfuni  31253  fourierdlem48  31483  fourierdlem49  31484  fourierdlem93  31528  resisresindm  31800  bnj1326  33179  bj-diagval  33695  pmodN  34664  polvalN  34719  polatN  34745  trnsetN  34970  djavalN  35950  dihmeetbclemN  36119  dihmeetlem11N  36132  djhval  36213  lclkrlem2e  36326  lcfrlem23  36380  lcdlss2N  36435  conrel2d  36800
  Copyright terms: Public domain W3C validator