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

Theorem ineq2d 3370
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 3364 . 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 1623    i^i cin 3151
This theorem is referenced by:  rint0  3902  riin0  3975  disji2  4010  disjprg  4019  disjxun  4021  onfr  4431  xpriindi  4822  riinint  4935  reseq2  4950  csbresg  4958  isofrlem  5837  isoselem  5838  oev2  6522  domss2  7020  kmlem11  7786  fpwwe2cbv  8252  fpwwe2lem3  8255  fpwwe2lem8  8259  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  fz1isolem  11399  limsupgle  11951  fsumm1  12216  incexclem  12295  bitsinv1  12633  bitsinvp1  12640  sadcadd  12649  sadadd2  12651  smumullem  12683  ressbas  13198  ressress  13205  restval  13331  ismred2  13505  resscatc  13937  cnvps  14321  cntziinsn  14810  lsmdisj3r  14995  lsmdisj3b  14999  dmdprd  15236  subgdmdprd  15269  pgpfaclem1  15316  subrgpropd  15579  crng2idl  15991  obselocv  16628  basis1  16688  baspartn  16692  eltg  16695  tgdom  16716  indistopon  16738  ntrval  16773  clslp  16879  resttopon2  16899  restopnb  16906  paste  17022  nrmsep3  17083  imacmp  17124  cmpsub  17127  llyi  17200  nllyi  17201  cldllycmp  17221  kgencmp2  17241  ptbasfi  17276  kqdisj  17423  kqcldsat  17424  trfbas2  17538  filss  17548  elfg  17566  flimclslem  17679  fcfneii  17732  tsmsfbas  17810  ressxms  18071  qtopbaslem  18267  pi1addf  18545  pi1addval  18546  shftmbl  18896  voliunlem1  18907  voliunlem2  18908  uniioombllem2  18938  uniioombllem4  18941  uniioombllem6  18943  volsup2  18960  volcn  18961  volivth  18962  itg1climres  19069  limciun  19244  dvres3a  19264  ig1pval  19558  issubgo  20970  omlsi  21983  pjoml  22015  chdmj3  22110  chdmj4  22111  ledi  22119  cmbr  22163  cmbr3  22187  pjoml3  22191  fh1  22197  fh2  22198  dmdbr  22879  dmdmd  22880  dmdbr5  22888  dmdsl3  22895  chirredlem2  22971  chirredlem3  22972  dmdbr6ati  23003  ballotlemfval  23048  fimacnvinrn  23199  fimacnvinrn2  23200  disji2f  23354  disjif2  23358  dfpo2  24112  predeq1  24169  predeq3  24171  predep  24192  moec  25047  splintx  25049  domrancur1c  25202  islimrs3  25581  islimrs4  25582  issubcat  25845  valtar  25883  indcls2  25996  pfsubkl  26047  topbnd  26242  opnbnd  26243  cldbnd  26244  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  neifg  26320  heiborlem3  26537  elrfi  26769  elrfirn  26770  elrfirn2  26771  eldioph2lem1  26839  bnj1326  29056  pmodN  30039  polvalN  30094  polatN  30120  trnsetN  30345  djavalN  31325  dihmeetbclemN  31494  dihmeetlem11N  31507  djhval  31588  lclkrlem2e  31701  lcfrlem23  31755  lcdlss2N  31810
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator