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

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

Proof of Theorem eleq2s
StepHypRef Expression
1 eleq2s.2 . . 3 𝐶 = 𝐵
21eleq2i 2120 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 118 1 (𝐴𝐶𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259   ∈ wcel 1409 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052 This theorem is referenced by:  elrabi  2718  opelopabsb  4025  epelg  4055  reg3exmidlemwe  4331  elxpi  4389  optocl  4444  fvmptss2  5275  fvmptssdm  5283  acexmidlemcase  5535  elmpt2cl  5726  mpt2xopn0yelv  5885  tfr2a  5967  2oconcl  6053  ecexr  6142  ectocld  6203  ecoptocl  6224  eroveu  6228  diffitest  6375  dmaddpqlem  6533  nqpi  6534  nq0nn  6598  0nsr  6892  axaddcl  6998  axmulcl  7000  peano2uzs  8623  fzossnn0  9133  rebtwn2zlemstep  9209  fldiv4p1lem1div2  9255  frecfzennn  9367  facnn  9595  bcpasc  9634  rexuz3  9817  rexanuz2  9818  r19.2uz  9820  cau4  9943  caubnd2  9944  climshft2  10058  climaddc1  10080  climmulc2  10082  climsubc1  10083  climsubc2  10084  climlec2  10092  climcau  10097  climcaucn  10101
 Copyright terms: Public domain W3C validator