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

Theorem ineq2d 3543
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 3537 . 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 1653    i^i cin 3320
This theorem is referenced by:  disjpr2  3871  rint0  4091  riin0  4165  disji2  4200  disjprg  4209  disjxun  4211  onfr  4621  xpriindi  5012  riinint  5127  reseq2  5142  csbresg  5150  isofrlem  6061  isoselem  6062  oev2  6768  domss2  7267  kmlem11  8041  fpwwe2cbv  8506  fpwwe2lem3  8509  fpwwe2lem8  8513  fpwwe2lem12  8517  fpwwe2lem13  8518  fpwwe2  8519  fz1isolem  11711  limsupgle  12272  fsumm1  12538  incexclem  12617  bitsinv1  12955  bitsinvp1  12962  sadcadd  12971  sadadd2  12973  smumullem  13005  ressbas  13520  ressress  13527  restval  13655  ismred2  13829  resscatc  14261  cnvps  14645  cntziinsn  15134  lsmdisj3r  15319  lsmdisj3b  15323  dmdprd  15560  subgdmdprd  15593  pgpfaclem1  15640  subrgpropd  15903  crng2idl  16311  obselocv  16956  basis1  17016  baspartn  17020  eltg  17023  tgdom  17044  indistopon  17066  ntrval  17101  clslp  17213  resttopon2  17233  restopnb  17240  paste  17359  nrmsep3  17420  imacmp  17461  cmpsub  17464  llyi  17538  nllyi  17539  cldllycmp  17559  kgencmp2  17579  ptbasfi  17614  kqdisj  17765  kqcldsat  17766  trfbas2  17876  filss  17886  elfg  17904  flimclslem  18017  fcfneii  18070  tsmsfbas  18158  restutopopn  18269  ressxms  18556  restmetu  18618  qtopbaslem  18793  pi1addf  19073  pi1addval  19074  shftmbl  19434  voliunlem1  19445  voliunlem2  19446  uniioombllem2  19476  uniioombllem4  19479  uniioombllem6  19481  volsup2  19498  volcn  19499  volivth  19500  itg1climres  19607  limciun  19782  dvres3a  19802  ig1pval  20096  2pthlem2  21597  issubgo  21892  omlsi  22907  pjoml  22939  chdmj3  23034  chdmj4  23035  ledi  23043  cmbr  23087  cmbr3  23111  pjoml3  23115  fh1  23121  fh2  23122  dmdbr  23803  dmdmd  23804  dmdbr5  23812  dmdsl3  23819  chirredlem2  23895  chirredlem3  23896  dmdbr6ati  23927  disji2f  24020  disjif2  24024  disjxpin  24029  fimacnvinrn  24048  fimacnvinrn2  24049  ballotlemfval  24748  dfpo2  25379  elima4  25405  predep  25468  mblfinlem2  26245  ftc1anclem6  26286  topbnd  26328  opnbnd  26329  cldbnd  26330  neibastop1  26389  neibastop2lem  26390  neibastop2  26391  neibastop3  26392  neifg  26401  heiborlem3  26523  elrfi  26749  elrfirn  26750  elrfirn2  26751  eldioph2lem1  26819  resisresindm  28075  frgrancvvdeqlem4  28423  bnj1326  29396  pmodN  30648  polvalN  30703  polatN  30729  trnsetN  30954  djavalN  31934  dihmeetbclemN  32103  dihmeetlem11N  32116  djhval  32197  lclkrlem2e  32310  lcfrlem23  32364  lcdlss2N  32419
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328
  Copyright terms: Public domain W3C validator