ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2s Unicode version

Theorem eleq2s 2259
Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
eleq2s.1  |-  ( A  e.  B  ->  ph )
eleq2s.2  |-  C  =  B
Assertion
Ref Expression
eleq2s  |-  ( A  e.  C  ->  ph )

Proof of Theorem eleq2s
StepHypRef Expression
1 eleq2s.2 . . 3  |-  C  =  B
21eleq2i 2231 . 2  |-  ( A  e.  C  <->  A  e.  B )
3 eleq2s.1 . 2  |-  ( A  e.  B  ->  ph )
42, 3sylbi 120 1  |-  ( A  e.  C  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1342    e. wcel 2135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160
This theorem is referenced by:  elrabi  2875  opelopabsb  4233  epelg  4263  reg3exmidlemwe  4551  elxpi  4615  optocl  4675  fvmptss2  5556  fvmptssdm  5565  acexmidlemcase  5832  elmpocl  6031  mpoxopn0yelv  6199  tfr2a  6281  tfri1dALT  6311  2oconcl  6399  el2oss1o  6403  ecexr  6498  ectocld  6559  ecoptocl  6580  eroveu  6584  mapsnconst  6652  diffitest  6845  en2eqpr  6865  ctssdccl  7068  exmidonfinlem  7141  exmidfodomrlemr  7150  exmidfodomrlemrALT  7151  dmaddpqlem  7310  nqpi  7311  nq0nn  7375  0nsr  7682  suplocsrlempr  7740  cnm  7765  axaddcl  7797  axmulcl  7799  aprcl  8536  peano2uzs  9514  fzssnn  9994  fzossnn0  10101  rebtwn2zlemstep  10179  fldiv4p1lem1div2  10231  frecfzennn  10352  fser0const  10442  facnn  10630  bcpasc  10669  hashfzo0  10726  rexuz3  10922  rexanuz2  10923  r19.2uz  10925  cau4  11048  caubnd2  11049  climshft2  11237  climaddc1  11260  climmulc2  11262  climsubc1  11263  climsubc2  11264  climlec2  11272  climcau  11278  climcaucn  11282  iserabs  11406  binomlem  11414  isumshft  11421  cvgratgt0  11464  clim2divap  11471  ntrivcvgap  11479  fprodntrivap  11515  fprodeq0  11548  infssuzex  11871  infssuzledc  11872  3prm  12049  phicl2  12135  phibndlem  12137  dfphi2  12141  crth  12145  phimullem  12146  znnen  12294  ennnfonelemkh  12308  bj-el2oss1o  13517  2o01f  13738  nninfalllem1  13750  nninfall  13751
  Copyright terms: Public domain W3C validator