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

Theorem ineq1d 3369
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 3363 . 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 1623    i^i cin 3151
This theorem is referenced by:  iinrab2  3965  disji2  4010  disjprg  4019  disjxun  4021  riinint  4935  fnresdisj  5354  fnimadisj  5364  ecinxp  6734  fiint  7133  fival  7166  marypha1lem  7186  kmlem12  7787  fin23lem12  7957  fin23lem30  7968  fin23lem33  7971  ttukeylem1  8136  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwe2  8265  fzval2  10785  limsupval  11948  limsupgval  11950  ello1  11989  elo1  12000  fsum1p  12218  incexclem  12295  smuval2  12673  smueqlem  12681  smumul  12684  isacs2  13555  acsfiel  13556  isacs1i  13559  catcval  13928  resscatc  13937  acsficl  14274  lsmdisj3  14992  lsmdisj3a  14998  dprdres  15263  dprdz  15265  dpjdisj  15288  lspdisj2  15880  indistopon  16738  restopnb  16906  ordtrest2  16934  isnrm  17063  cmpcov  17116  cmpsublem  17126  cmpsub  17127  tgcmp  17128  uncmp  17130  hauscmplem  17133  nconsubb  17149  isnlly  17195  kgeni  17232  kgencn3  17253  ptcld  17307  ptcnplem  17315  alexsublem  17738  alexsubb  17740  alexsubALTlem2  17742  alexsubALTlem4  17744  alexsubALT  17745  tmdgsum2  17779  tsmsval2  17812  metrest  18070  qtopbaslem  18267  cnheibor  18453  bndth  18456  lebnumii  18464  iscph  18606  csscld  18676  clsocv  18677  ovolicc2  18881  voliunlem3  18909  ioombl  18922  uniioombllem2  18938  uniioombllem4  18941  uniioombllem6  18943  mbflimsup  19021  taylfval  19738  chtval  20348  ppival  20365  ppival2  20366  ppival2g  20367  chtfl  20387  ppiprm  20389  chtprm  20391  chtnprm  20392  chtdif  20396  ppidif  20401  prmorcht  20416  chdmj2  22109  cmcmlem  22170  pjoml2  22190  fh2  22198  mdbr  22874  mdi  22875  mdbr3  22877  mdbr4  22878  dmdmd  22880  dmdbr3  22885  dmdbr4  22886  dmdi4  22887  dmdbr5  22888  mddmd2  22889  mdsl1i  22901  cvmdi  22904  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd1lem3  22907  mdslmd1lem4  22908  mdslmd1i  22909  mdslmd3i  22912  csmdsymi  22914  mdexchi  22915  atomli  22962  atabsi  22981  sumdmdlem2  22999  dmdbr5ati  23002  ballotlemfval  23048  ballotlemfp1  23050  ballotlemgun  23083  disji2f  23354  disjif2  23358  totprobd  23629  probmeasb  23633  iccllyscon  23781  limsucncmpi  24884  mapex2  25140  bwt2  25592  vtarsu  25886  selsubf3g  25992  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibg2aalem2  26114  lppotos  26144  bsstrs  26146  nbssntrs  26147  isside0  26164  isside1  26165  bosser  26167  pdiveql  26168  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  sstotbnd2  26498  cntotbnd  26520  heibor  26545  fninfp  26754  elrfi  26769  isnacs  26779  mrefg2  26782  mapfzcons2  26796  coeq0i  26832  eldioph2lem2  26840  aomclem8  27159  kelac1  27161  islmodfg  27167  lnr2i  27320  fgraphopab  27529  stoweidlem50  27799  stoweidlem57  27806  diftpsneq  28070  bnj1385  28865  bnj1326  29056  l1cvat  29245  pmodlem2  30036  pmod2iN  30038  hlmod1i  30045  osumcllem3N  30147  osumcllem9N  30153  pexmidlem6N  30164  pl42lem1N  30168  istrnN  30346  djavalN  31325  dihmeetlem9N  31505  dihmeetlem11N  31507  dihmeetlem12N  31508  dihoml4  31567  djhval  31588  dochexmidlem6  31655  lclkrlem2b  31698  lcfrlem20  31752  lcfrlem23  31755
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