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

Theorem ineq2d 3446
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 3440 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2syl 15 1  |-  ( ph  ->  ( C  i^i  A
)  =  ( C  i^i  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    i^i cin 3227
This theorem is referenced by:  rint0  3981  riin0  4054  disji2  4089  disjprg  4098  disjxun  4100  onfr  4510  xpriindi  4901  riinint  5014  reseq2  5029  csbresg  5037  isofrlem  5921  isoselem  5922  oev2  6606  domss2  7105  kmlem11  7873  fpwwe2cbv  8339  fpwwe2lem3  8342  fpwwe2lem8  8346  fpwwe2lem12  8350  fpwwe2lem13  8351  fpwwe2  8352  fz1isolem  11489  limsupgle  12041  fsumm1  12307  incexclem  12386  bitsinv1  12724  bitsinvp1  12731  sadcadd  12740  sadadd2  12742  smumullem  12774  ressbas  13289  ressress  13296  restval  13424  ismred2  13598  resscatc  14030  cnvps  14414  cntziinsn  14903  lsmdisj3r  15088  lsmdisj3b  15092  dmdprd  15329  subgdmdprd  15362  pgpfaclem1  15409  subrgpropd  15672  crng2idl  16084  obselocv  16728  basis1  16788  baspartn  16792  eltg  16795  tgdom  16816  indistopon  16838  ntrval  16873  clslp  16979  resttopon2  16999  restopnb  17006  paste  17122  nrmsep3  17183  imacmp  17224  cmpsub  17227  llyi  17300  nllyi  17301  cldllycmp  17321  kgencmp2  17341  ptbasfi  17376  kqdisj  17523  kqcldsat  17524  trfbas2  17634  filss  17644  elfg  17662  flimclslem  17775  fcfneii  17828  tsmsfbas  17906  ressxms  18167  qtopbaslem  18363  pi1addf  18643  pi1addval  18644  shftmbl  18994  voliunlem1  19005  voliunlem2  19006  uniioombllem2  19036  uniioombllem4  19039  uniioombllem6  19041  volsup2  19058  volcn  19059  volivth  19060  itg1climres  19167  limciun  19342  dvres3a  19362  ig1pval  19656  issubgo  21076  omlsi  22091  pjoml  22123  chdmj3  22218  chdmj4  22219  ledi  22227  cmbr  22271  cmbr3  22295  pjoml3  22299  fh1  22305  fh2  22306  dmdbr  22987  dmdmd  22988  dmdbr5  22996  dmdsl3  23003  chirredlem2  23079  chirredlem3  23080  dmdbr6ati  23111  disji2f  23215  disjif2  23219  fimacnvinrn  23248  fimacnvinrn2  23249  restutopopn  23542  restmetu  23615  ballotlemfval  23996  dfpo2  24670  predeq1  24727  predeq3  24729  predep  24750  topbnd  25566  opnbnd  25567  cldbnd  25568  neibastop1  25632  neibastop2lem  25633  neibastop2  25634  neibastop3  25635  neifg  25644  heiborlem3  25860  elrfi  26092  elrfirn  26093  elrfirn2  26094  eldioph2lem1  26162  disjpr2  27409  2pthonlem2  27719  frgrancvvdeqlem4  27849  bnj1326  28801  pmodN  30091  polvalN  30146  polatN  30172  trnsetN  30397  djavalN  31377  dihmeetbclemN  31546  dihmeetlem11N  31559  djhval  31640  lclkrlem2e  31753  lcfrlem23  31807  lcdlss2N  31862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235
  Copyright terms: Public domain W3C validator