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

Theorem eleq2s 2132
 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 2104 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 114 1 (𝐴𝐶𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393 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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036 This theorem is referenced by:  elrabi  2695  opelopabsb  3997  epelg  4027  reg3exmidlemwe  4303  elxpi  4361  optocl  4416  fvmptss2  5247  fvmptssdm  5255  acexmidlemcase  5507  elmpt2cl  5698  mpt2xopn0yelv  5854  tfr2a  5936  2oconcl  6022  ecexr  6111  ectocld  6172  ecoptocl  6193  eroveu  6197  diffitest  6344  dmaddpqlem  6475  nqpi  6476  nq0nn  6540  0nsr  6834  axaddcl  6940  axmulcl  6942  peano2uzs  8527  fzossnn0  9031  rebtwn2zlemstep  9107  fldiv4p1lem1div2  9147  frecfzennn  9203  rexuz3  9588  rexanuz2  9589  r19.2uz  9591  cau4  9712  caubnd2  9713  climshft2  9827  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  climlec2  9861  climcau  9866  climcaucn  9870
 Copyright terms: Public domain W3C validator