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

Theorem ineq1d 3382
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
ineq1d  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  C ) )

Proof of Theorem ineq1d
StepHypRef Expression
1 ineq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ineq1 3376 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
31, 2syl 15 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    i^i cin 3164
This theorem is referenced by:  diftpsn3  3772  iinrab2  3981  disji2  4026  disjprg  4035  disjxun  4037  riinint  4951  fnresdisj  5370  fnimadisj  5380  ecinxp  6750  fiint  7149  fival  7182  marypha1lem  7202  kmlem12  7803  fin23lem12  7973  fin23lem30  7984  fin23lem33  7987  ttukeylem1  8152  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwe2  8281  fzval2  10801  limsupval  11964  limsupgval  11966  ello1  12005  elo1  12016  fsum1p  12234  incexclem  12311  smuval2  12689  smueqlem  12697  smumul  12700  isacs2  13571  acsfiel  13572  isacs1i  13575  catcval  13944  resscatc  13953  acsficl  14290  lsmdisj3  15008  lsmdisj3a  15014  dprdres  15279  dprdz  15281  dpjdisj  15304  lspdisj2  15896  indistopon  16754  restopnb  16922  ordtrest2  16950  isnrm  17079  cmpcov  17132  cmpsublem  17142  cmpsub  17143  tgcmp  17144  uncmp  17146  hauscmplem  17149  nconsubb  17165  isnlly  17211  kgeni  17248  kgencn3  17269  ptcld  17323  ptcnplem  17331  alexsublem  17754  alexsubb  17756  alexsubALTlem2  17758  alexsubALTlem4  17760  alexsubALT  17761  tmdgsum2  17795  tsmsval2  17828  metrest  18086  qtopbaslem  18283  cnheibor  18469  bndth  18472  lebnumii  18480  iscph  18622  csscld  18692  clsocv  18693  ovolicc2  18897  voliunlem3  18925  ioombl  18938  uniioombllem2  18954  uniioombllem4  18957  uniioombllem6  18959  mbflimsup  19037  taylfval  19754  chtval  20364  ppival  20381  ppival2  20382  ppival2g  20383  chtfl  20403  ppiprm  20405  chtprm  20407  chtnprm  20408  chtdif  20412  ppidif  20417  prmorcht  20432  chdmj2  22125  cmcmlem  22186  pjoml2  22206  fh2  22214  mdbr  22890  mdi  22891  mdbr3  22893  mdbr4  22894  dmdmd  22896  dmdbr3  22901  dmdbr4  22902  dmdi4  22903  dmdbr5  22904  mddmd2  22905  mdsl1i  22917  cvmdi  22920  mdslmd1lem1  22921  mdslmd1lem2  22922  mdslmd1lem3  22923  mdslmd1lem4  22924  mdslmd1i  22925  mdslmd3i  22928  csmdsymi  22930  mdexchi  22931  atomli  22978  atabsi  22997  sumdmdlem2  23015  dmdbr5ati  23018  ballotlemfval  23064  ballotlemfp1  23066  ballotlemgun  23099  disji2f  23369  disjif2  23373  totprobd  23644  probmeasb  23648  iccllyscon  23796  limsucncmpi  24956  mapex2  25243  bwt2  25695  vtarsu  25989  selsubf3g  26095  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  lppotos  26247  bsstrs  26249  nbssntrs  26250  isside0  26267  isside1  26268  bosser  26270  pdiveql  26271  neibastop2lem  26412  neibastop2  26413  neibastop3  26414  sstotbnd2  26601  cntotbnd  26623  heibor  26648  fninfp  26857  elrfi  26872  isnacs  26882  mrefg2  26885  mapfzcons2  26899  coeq0i  26935  eldioph2lem2  26943  aomclem8  27262  kelac1  27264  islmodfg  27270  lnr2i  27423  fgraphopab  27632  stoweidlem50  27902  stoweidlem57  27909  injresinjlem  28214  bnj1385  29181  bnj1326  29372  l1cvat  29867  pmodlem2  30658  pmod2iN  30660  hlmod1i  30667  osumcllem3N  30769  osumcllem9N  30775  pexmidlem6N  30786  pl42lem1N  30790  istrnN  30968  djavalN  31947  dihmeetlem9N  32127  dihmeetlem11N  32129  dihmeetlem12N  32130  dihoml4  32189  djhval  32210  dochexmidlem6  32277  lclkrlem2b  32320  lcfrlem20  32374  lcfrlem23  32377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator