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

Theorem ineq1d 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
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 3537 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    i^i cin 3321
This theorem is referenced by:  diftpsn3  3939  iinrab2  4156  disji2  4201  disjprg  4210  disjxun  4212  riinint  5128  fnresdisj  5557  fnimadisj  5567  ecinxp  6981  fiint  7385  fival  7419  marypha1lem  7440  kmlem12  8043  fin23lem12  8213  fin23lem30  8224  fin23lem33  8227  ttukeylem1  8391  fpwwe2cbv  8507  fpwwe2lem2  8509  fpwwe2  8520  fzval2  11048  injresinjlem  11201  limsupval  12270  limsupgval  12272  ello1  12311  elo1  12322  fsum1p  12541  incexclem  12618  smuval2  12996  smueqlem  13004  smumul  13007  isacs2  13880  acsfiel  13881  isacs1i  13884  catcval  14253  resscatc  14262  acsficl  14599  lsmdisj3  15317  lsmdisj3a  15323  dprdres  15588  dprdz  15590  dpjdisj  15613  lspdisj2  16201  indistopon  17067  restopnb  17241  ordtrest2  17270  isnrm  17401  cmpcov  17454  cmpsublem  17464  cmpsub  17465  tgcmp  17466  uncmp  17468  hauscmplem  17471  bwth  17475  nconsubb  17488  isnlly  17534  kgeni  17571  kgencn3  17592  ptcld  17647  ptcnplem  17655  alexsublem  18077  alexsubb  18079  alexsubALTlem2  18081  alexsubALTlem4  18083  alexsubALT  18084  tmdgsum2  18128  tsmsval2  18161  ustexsym  18247  metrest  18556  qtopbaslem  18794  cnheibor  18982  bndth  18985  lebnumii  18993  iscph  19135  csscld  19205  clsocv  19206  ovolicc2  19420  voliunlem3  19448  ioombl  19461  uniioombllem2  19477  uniioombllem4  19480  uniioombllem6  19482  mbflimsup  19560  taylfval  20277  chtval  20895  ppival  20912  ppival2  20913  ppival2g  20914  chtfl  20934  ppiprm  20936  chtprm  20938  chtnprm  20939  chtdif  20943  ppidif  20948  prmorcht  20963  2pthlem2  21598  chdmj2  23034  cmcmlem  23095  pjoml2  23115  fh2  23123  mdbr  23799  mdi  23800  mdbr3  23802  mdbr4  23803  dmdmd  23805  dmdbr3  23810  dmdbr4  23811  dmdi4  23812  dmdbr5  23813  mddmd2  23814  mdsl1i  23826  cvmdi  23829  mdslmd1lem1  23830  mdslmd1lem2  23831  mdslmd1lem3  23832  mdslmd1lem4  23833  mdslmd1i  23834  mdslmd3i  23837  csmdsymi  23839  mdexchi  23840  atomli  23887  atabsi  23906  sumdmdlem2  23924  dmdbr5ati  23927  disji2f  24021  disjif2  24025  disjxpin  24030  totprobd  24686  probmeasb  24690  ballotlemfval  24749  ballotlemfp1  24751  ballotlemgun  24784  iccllyscon  24939  fprod1p  25293  limsucncmpi  26197  mblfinlem2  26246  neibastop2lem  26391  neibastop2  26392  neibastop3  26393  sstotbnd2  26485  cntotbnd  26507  heibor  26532  fninfp  26737  elrfi  26750  isnacs  26760  mrefg2  26763  mapfzcons2  26777  coeq0i  26813  eldioph2lem2  26821  aomclem8  27138  kelac1  27140  islmodfg  27146  lnr2i  27299  fgraphopab  27508  stoweidlem50  27777  stoweidlem57  27784  frgrancvvdeqlem4  28484  bnj1385  29266  bnj1326  29457  l1cvat  29915  pmodlem2  30706  pmod2iN  30708  hlmod1i  30715  osumcllem3N  30817  osumcllem9N  30823  pexmidlem6N  30834  pl42lem1N  30838  istrnN  31016  djavalN  31995  dihmeetlem9N  32175  dihmeetlem11N  32177  dihmeetlem12N  32178  dihoml4  32237  djhval  32258  dochexmidlem6  32325  lclkrlem2b  32368  lcfrlem20  32422  lcfrlem23  32425
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 2419
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329
  Copyright terms: Public domain W3C validator