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

Theorem eleq2s 2234
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 2206 . 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 1331    e. wcel 1480
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  elrabi  2837  opelopabsb  4182  epelg  4212  reg3exmidlemwe  4493  elxpi  4555  optocl  4615  fvmptss2  5496  fvmptssdm  5505  acexmidlemcase  5769  elmpocl  5968  mpoxopn0yelv  6136  tfr2a  6218  tfri1dALT  6248  2oconcl  6336  ecexr  6434  ectocld  6495  ecoptocl  6516  eroveu  6520  mapsnconst  6588  diffitest  6781  en2eqpr  6801  ctssdccl  6996  exmidonfinlem  7049  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  dmaddpqlem  7192  nqpi  7193  nq0nn  7257  0nsr  7564  suplocsrlempr  7622  cnm  7647  axaddcl  7679  axmulcl  7681  aprcl  8415  peano2uzs  9386  fzssnn  9855  fzossnn0  9959  rebtwn2zlemstep  10037  fldiv4p1lem1div2  10085  frecfzennn  10206  fser0const  10296  facnn  10480  bcpasc  10519  hashfzo0  10576  rexuz3  10769  rexanuz2  10770  r19.2uz  10772  cau4  10895  caubnd2  10896  climshft2  11082  climaddc1  11105  climmulc2  11107  climsubc1  11108  climsubc2  11109  climlec2  11117  climcau  11123  climcaucn  11127  iserabs  11251  binomlem  11259  isumshft  11266  cvgratgt0  11309  clim2divap  11316  ntrivcvgap  11324  infssuzex  11649  infssuzledc  11650  3prm  11816  phicl2  11897  phibndlem  11899  dfphi2  11903  crth  11907  phimullem  11908  znnen  11918  ennnfonelemkh  11932  bj-el2oss1o  13011  el2oss1o  13218  nninfalllem1  13233  nninfall  13234  isomninnlem  13255
  Copyright terms: Public domain W3C validator