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

Theorem ineq2d 3550
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 3544 . 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 1369    i^i cin 3325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3333
This theorem is referenced by:  disjpr2  3936  rint0  4166  riin0  4242  disji2  4277  disjprg  4286  disjxun  4288  onfr  4756  xpriindi  4974  riinint  5094  reseq2  5103  csbresgOLD  5112  resindm  5149  isofrlem  6029  isoselem  6030  oev2  6961  domss2  7468  funsnfsupp  7642  kmlem11  8327  fpwwe2cbv  8795  fpwwe2lem3  8798  fpwwe2lem8  8802  fpwwe2lem12  8806  fpwwe2lem13  8807  fpwwe2  8808  fz1isolem  12212  limsupgle  12953  fsumm1  13218  incexclem  13297  bitsinv1  13636  bitsinvp1  13643  sadcadd  13652  sadadd2  13654  smumullem  13686  ressbas  14226  ressress  14233  restval  14363  ismred2  14539  resscatc  14971  cnvps  15380  cntziinsn  15850  lsmdisj3r  16181  lsmdisj3b  16185  dmdprd  16478  subgdmdprd  16529  pgpfaclem1  16580  srgbinomlem4  16639  subrgpropd  16897  crng2idl  17319  obselocv  18151  basis1  18553  baspartn  18557  eltg  18560  tgdom  18581  indistopon  18603  ntrval  18638  clslp  18750  resttopon2  18770  restopnb  18777  paste  18896  nrmsep3  18957  imacmp  18998  cmpsub  19001  bwth  19011  llyi  19076  nllyi  19077  cldllycmp  19097  kgencmp2  19117  ptbasfi  19152  kqdisj  19303  kqcldsat  19304  trfbas2  19414  filss  19424  elfg  19442  flimclslem  19555  fcfneii  19608  tsmsfbas  19696  restutopopn  19811  ressxms  20098  restmetu  20160  qtopbaslem  20335  pi1addf  20617  pi1addval  20618  shftmbl  21018  voliunlem1  21029  voliunlem2  21030  uniioombllem2  21061  uniioombllem4  21064  uniioombllem6  21066  volsup2  21083  volcn  21084  volivth  21085  itg1climres  21190  limciun  21367  dvres3a  21387  ig1pval  21642  2pthlem2  23493  issubgo  23788  omlsi  24805  pjoml  24837  chdmj3  24932  chdmj4  24933  ledi  24941  cmbr  24985  cmbr3  25009  pjoml3  25013  fh1  25019  fh2  25020  dmdbr  25701  dmdmd  25702  dmdbr5  25710  dmdsl3  25717  chirredlem2  25793  chirredlem3  25794  dmdbr6ati  25825  disji2f  25919  disjif2  25923  disjxpin  25928  disjunsn  25934  fimacnvinrn  25950  fimacnvinrn2  25951  prsss  26344  ordtrestNEW  26349  ballotlemfval  26870  signsplypnf  26949  dfpo2  27563  elima4  27588  predep  27651  mblfinlem2  28426  ftc1anclem6  28469  topbnd  28516  opnbnd  28517  cldbnd  28518  neibastop1  28577  neibastop2lem  28578  neibastop2  28579  neibastop3  28580  neifg  28589  heiborlem3  28709  elrfi  29027  elrfirn  29028  elrfirn2  29029  eldioph2lem1  29095  resisresindm  30136  frgrancvvdeqlem4  30623  bnj1326  32014  bj-diagval  32522  pmodN  33491  polvalN  33546  polatN  33572  trnsetN  33797  djavalN  34777  dihmeetbclemN  34946  dihmeetlem11N  34959  djhval  35040  lclkrlem2e  35153  lcfrlem23  35207  lcdlss2N  35262
  Copyright terms: Public domain W3C validator