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

Theorem eleq2s 2174
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 2146 . 2  |-  ( A  e.  C  <->  A  e.  B )
3 eleq2s.1 . 2  |-  ( A  e.  B  ->  ph )
42, 3sylbi 119 1  |-  ( A  e.  C  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285    e. wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  elrabi  2747  opelopabsb  4023  epelg  4053  reg3exmidlemwe  4329  elxpi  4387  optocl  4442  fvmptss2  5279  fvmptssdm  5287  acexmidlemcase  5538  elmpt2cl  5729  mpt2xopn0yelv  5888  tfr2a  5970  tfri1dALT  6000  2oconcl  6086  ecexr  6177  ectocld  6238  ecoptocl  6259  eroveu  6263  diffitest  6421  en2eqpr  6434  dmaddpqlem  6629  nqpi  6630  nq0nn  6694  0nsr  6988  axaddcl  7094  axmulcl  7096  peano2uzs  8753  fzossnn0  9261  rebtwn2zlemstep  9339  fldiv4p1lem1div2  9387  frecfzennn  9508  facnn  9751  bcpasc  9790  rexuz3  10014  rexanuz2  10015  r19.2uz  10017  cau4  10140  caubnd2  10141  climshft2  10283  climaddc1  10305  climmulc2  10307  climsubc1  10308  climsubc2  10309  climlec2  10317  climcau  10322  climcaucn  10326  infssuzex  10489  infssuzledc  10490  3prm  10654  znnen  10709
  Copyright terms: Public domain W3C validator