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

Theorem ineq2d 3664
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 3658 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2syl 17 1  |-  ( ph  ->  ( C  i^i  A
)  =  ( C  i^i  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    i^i cin 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443
This theorem is referenced by:  disjpr2  4062  rint0  4296  riin0  4373  disji2  4410  disjprg  4419  disjxun  4421  xpriindi  4990  riinint  5110  reseq2  5119  resindm  5168  predep  5425  onfr  5481  isofrlem  6246  isoselem  6247  oev2  7236  domss2  7740  funsnfsupp  7916  kmlem11  8597  fpwwe2cbv  9062  fpwwe2lem3  9065  fpwwe2lem8  9069  fpwwe2lem12  9073  fpwwe2lem13  9074  fpwwe2  9075  fz1isolem  12628  limsupgle  13534  fsumm1  13811  incexclem  13893  bitsinv1  14415  bitsinvp1  14422  sadcadd  14431  sadadd2  14433  smumullem  14465  ressbas  15178  ressress  15186  restval  15324  ismred2  15508  resscatc  15999  cnvps  16457  cntziinsn  16987  lsmdisj3r  17335  lsmdisj3b  17339  gsummptfzsplitl  17565  dmdprd  17629  subgdmdprd  17666  pgpfaclem1  17713  subrgpropd  18041  crng2idl  18462  obselocv  19289  basis1  19963  baspartn  19967  eltg  19970  tgdom  19992  indistopon  20014  ntrval  20049  clslp  20162  resttopon2  20182  restopnb  20189  paste  20308  nrmsep3  20369  imacmp  20410  cmpsub  20413  bwth  20423  llyi  20487  nllyi  20488  cldllycmp  20508  kgencmp2  20559  ptbasfi  20594  kqdisj  20745  kqcldsat  20746  trfbas2  20856  filss  20866  elfg  20884  flimclslem  20997  fcfneii  21050  tsmsfbas  21140  restutopopn  21251  ressxms  21538  restmetu  21583  qtopbaslem  21777  pi1addf  22076  pi1addval  22077  shftmbl  22490  voliunlem1  22501  voliunlem2  22502  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem4  22542  uniioombllem6  22544  volsup2  22561  volcn  22562  volivth  22563  itg1climres  22670  limciun  22847  dvres3a  22867  ig1pval  23122  ig1pvalOLD  23128  2pthlem2  25324  frgrancvvdeqlem4  25759  issubgo  26029  omlsi  27055  pjoml  27087  chdmj3  27182  chdmj4  27183  ledi  27191  cmbr  27235  cmbr3  27259  pjoml3  27263  fh1  27269  fh2  27270  dmdbr  27950  dmdmd  27951  dmdbr5  27959  dmdsl3  27966  chirredlem2  28042  chirredlem3  28043  dmdbr6ati  28074  disji2f  28189  disjif2  28193  disjxpin  28200  disjunsn  28206  fimacnvinrn  28237  fimacnvinrn2  28238  prsss  28730  carsgclctunlem1  29157  carsgclctunlem2  29159  carsgclctunlem3  29160  ballotlemfval  29330  signsplypnf  29447  bnj1326  29843  mvrsval  30151  msrfval  30183  mthmpps  30228  dfpo2  30402  elima4  30428  topbnd  30985  opnbnd  30986  cldbnd  30987  neibastop1  31020  neibastop2lem  31021  neibastop2  31022  neibastop3  31023  neifg  31032  bj-diagval  31609  csbpredg  31691  poimirlem3  31907  mblfinlem2  31942  ftc1anclem6  31986  heiborlem3  32109  pmodN  33384  polvalN  33439  polatN  33465  trnsetN  33691  djavalN  34672  dihmeetbclemN  34841  dihmeetlem11N  34854  djhval  34935  lclkrlem2e  35048  lcfrlem23  35102  lcdlss2N  35157  elrfi  35505  elrfirn  35506  elrfirn2  35507  eldioph2lem1  35571  conrel2d  36226  csbresgOLD  37189  inabs3  37369  disjiun2  37371  fresin2  37396  lptioo2  37651  lptioo1  37652  cncfuni  37704  fourierdlem48  37958  fourierdlem49  37959  fourierdlem93  38003  nnfoctbdjlem  38201  carageniuncllem1  38250  carageniuncllem2  38251  resisresindm  38875
  Copyright terms: Public domain W3C validator