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

Theorem ineq2d 3686
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 3680 . 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 1398    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468
This theorem is referenced by:  disjpr2  4078  rint0  4312  riin0  4389  disji2  4426  disjprg  4435  disjxun  4437  onfr  4906  xpriindi  5128  riinint  5248  reseq2  5257  resindm  5306  isofrlem  6211  isoselem  6212  oev2  7165  domss2  7669  funsnfsupp  7845  kmlem11  8531  fpwwe2cbv  8997  fpwwe2lem3  9000  fpwwe2lem8  9004  fpwwe2lem12  9008  fpwwe2lem13  9009  fpwwe2  9010  fz1isolem  12497  limsupgle  13385  fsumm1  13651  incexclem  13733  bitsinv1  14179  bitsinvp1  14186  sadcadd  14195  sadadd2  14197  smumullem  14229  ressbas  14776  ressress  14784  restval  14919  ismred2  15095  resscatc  15586  cnvps  16044  cntziinsn  16574  lsmdisj3r  16906  lsmdisj3b  16910  gsummptfzsplitl  17154  dmdprd  17227  subgdmdprd  17279  pgpfaclem1  17330  subrgpropd  17661  crng2idl  18085  obselocv  18935  basis1  19621  baspartn  19625  eltg  19628  tgdom  19650  indistopon  19672  ntrval  19707  clslp  19819  resttopon2  19839  restopnb  19846  paste  19965  nrmsep3  20026  imacmp  20067  cmpsub  20070  bwth  20080  llyi  20144  nllyi  20145  cldllycmp  20165  kgencmp2  20216  ptbasfi  20251  kqdisj  20402  kqcldsat  20403  trfbas2  20513  filss  20523  elfg  20541  flimclslem  20654  fcfneii  20707  tsmsfbas  20795  restutopopn  20910  ressxms  21197  restmetu  21259  qtopbaslem  21434  pi1addf  21716  pi1addval  21717  shftmbl  22118  voliunlem1  22129  voliunlem2  22130  uniioombllem2  22161  uniioombllem4  22164  uniioombllem6  22166  volsup2  22183  volcn  22184  volivth  22185  itg1climres  22290  limciun  22467  dvres3a  22487  ig1pval  22742  2pthlem2  24803  frgrancvvdeqlem4  25238  issubgo  25506  omlsi  26523  pjoml  26555  chdmj3  26650  chdmj4  26651  ledi  26659  cmbr  26703  cmbr3  26727  pjoml3  26731  fh1  26737  fh2  26738  dmdbr  27419  dmdmd  27420  dmdbr5  27428  dmdsl3  27435  chirredlem2  27511  chirredlem3  27512  dmdbr6ati  27543  disji2f  27651  disjif2  27655  disjxpin  27661  disjunsn  27667  fimacnvinrn  27699  fimacnvinrn2  27700  prsss  28136  carsgclctunlem1  28528  carsgclctunlem2  28530  carsgclctunlem3  28531  ballotlemfval  28695  signsplypnf  28774  mvrsval  29132  msrfval  29164  mthmpps  29209  dfpo2  29428  elima4  29452  predep  29515  mblfinlem2  30295  ftc1anclem6  30338  topbnd  30385  opnbnd  30386  cldbnd  30387  neibastop1  30420  neibastop2lem  30421  neibastop2  30422  neibastop3  30423  neifg  30432  heiborlem3  30552  elrfi  30869  elrfirn  30870  elrfirn2  30871  eldioph2lem1  30935  fresin2  31691  lptioo2  31879  lptioo1  31880  cncfuni  31931  fourierdlem48  32179  fourierdlem49  32180  fourierdlem93  32224  resisresindm  32698  csbresgOLD  34039  bnj1326  34502  bj-diagval  35025  pmodN  35990  polvalN  36045  polatN  36071  trnsetN  36297  djavalN  37278  dihmeetbclemN  37447  dihmeetlem11N  37460  djhval  37541  lclkrlem2e  37654  lcfrlem23  37708  lcdlss2N  37763  conrel2d  38196
  Copyright terms: Public domain W3C validator