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

Theorem eleq2s 2110
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 2082 . 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 1226   wcel 1370
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 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011  df-clel 2014
This theorem is referenced by:  elrabi  2668  opelopabsb  3967  epelg  3997  elxpi  4284  optocl  4339  fvmptss2  5168  fvmptssdm  5176  acexmidlemcase  5427  elmpt2cl  5617  mpt2xopn0yelv  5772  tfr2a  5854  2oconcl  5933  ecexr  6018  ectocld  6079  ecoptocl  6100  eroveu  6104  dmaddpqlem  6230  nqpi  6231  nq0nn  6291  0nsr  6493  axaddcl  6559  axmulcl  6561
  Copyright terms: Public domain W3C validator