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

Theorem eleq2s 2129
Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
eleq2s.1 (A Bφ)
eleq2s.2 𝐶 = B
Assertion
Ref Expression
eleq2s (A 𝐶φ)

Proof of Theorem eleq2s
StepHypRef Expression
1 eleq2s.2 . . 3 𝐶 = B
21eleq2i 2101 . 2 (A 𝐶A B)
3 eleq2s.1 . 2 (A Bφ)
42, 3sylbi 114 1 (A 𝐶φ)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   wcel 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033
This theorem is referenced by:  elrabi  2689  opelopabsb  3988  epelg  4018  elxpi  4304  optocl  4359  fvmptss2  5190  fvmptssdm  5198  acexmidlemcase  5450  elmpt2cl  5640  mpt2xopn0yelv  5795  tfr2a  5877  2oconcl  5961  ecexr  6047  ectocld  6108  ecoptocl  6129  eroveu  6133  dmaddpqlem  6361  nqpi  6362  nq0nn  6424  0nsr  6657  axaddcl  6730  axmulcl  6732  peano2uzs  8283  fzossnn0  8781  frecfzennn  8864
  Copyright terms: Public domain W3C validator