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

Theorem ineq2d 3510
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 3504 . 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 set class
Syntax hints:    -> wi 4    = wceq 1649    i^i cin 3287
This theorem is referenced by:  disjpr2  3838  rint0  4058  riin0  4132  disji2  4167  disjprg  4176  disjxun  4178  onfr  4588  xpriindi  4978  riinint  5093  reseq2  5108  csbresg  5116  isofrlem  6027  isoselem  6028  oev2  6734  domss2  7233  kmlem11  8004  fpwwe2cbv  8469  fpwwe2lem3  8472  fpwwe2lem8  8476  fpwwe2lem12  8480  fpwwe2lem13  8481  fpwwe2  8482  fz1isolem  11673  limsupgle  12234  fsumm1  12500  incexclem  12579  bitsinv1  12917  bitsinvp1  12924  sadcadd  12933  sadadd2  12935  smumullem  12967  ressbas  13482  ressress  13489  restval  13617  ismred2  13791  resscatc  14223  cnvps  14607  cntziinsn  15096  lsmdisj3r  15281  lsmdisj3b  15285  dmdprd  15522  subgdmdprd  15555  pgpfaclem1  15602  subrgpropd  15865  crng2idl  16273  obselocv  16918  basis1  16978  baspartn  16982  eltg  16985  tgdom  17006  indistopon  17028  ntrval  17063  clslp  17174  resttopon2  17194  restopnb  17201  paste  17320  nrmsep3  17381  imacmp  17422  cmpsub  17425  llyi  17498  nllyi  17499  cldllycmp  17519  kgencmp2  17539  ptbasfi  17574  kqdisj  17725  kqcldsat  17726  trfbas2  17836  filss  17846  elfg  17864  flimclslem  17977  fcfneii  18030  tsmsfbas  18118  restutopopn  18229  ressxms  18516  restmetu  18578  qtopbaslem  18753  pi1addf  19033  pi1addval  19034  shftmbl  19394  voliunlem1  19405  voliunlem2  19406  uniioombllem2  19436  uniioombllem4  19439  uniioombllem6  19441  volsup2  19458  volcn  19459  volivth  19460  itg1climres  19567  limciun  19742  dvres3a  19762  ig1pval  20056  2pthlem2  21557  issubgo  21852  omlsi  22867  pjoml  22899  chdmj3  22994  chdmj4  22995  ledi  23003  cmbr  23047  cmbr3  23071  pjoml3  23075  fh1  23081  fh2  23082  dmdbr  23763  dmdmd  23764  dmdbr5  23772  dmdsl3  23779  chirredlem2  23855  chirredlem3  23856  dmdbr6ati  23887  disji2f  23980  disjif2  23984  disjxpin  23989  fimacnvinrn  24008  fimacnvinrn2  24009  ballotlemfval  24708  dfpo2  25334  predeq1  25391  predeq3  25393  predep  25414  mblfinlem  26151  topbnd  26225  opnbnd  26226  cldbnd  26227  neibastop1  26286  neibastop2lem  26287  neibastop2  26288  neibastop3  26289  neifg  26298  heiborlem3  26420  elrfi  26646  elrfirn  26647  elrfirn2  26648  eldioph2lem1  26716  resisresindm  27965  frgrancvvdeqlem4  28144  bnj1326  29113  pmodN  30344  polvalN  30399  polatN  30425  trnsetN  30650  djavalN  31630  dihmeetbclemN  31799  dihmeetlem11N  31812  djhval  31893  lclkrlem2e  32006  lcfrlem23  32060  lcdlss2N  32115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295
  Copyright terms: Public domain W3C validator