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

Theorem eleq2s 2210
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 2182 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 120 1 (𝐴𝐶𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wcel 1463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  elrabi  2808  opelopabsb  4150  epelg  4180  reg3exmidlemwe  4461  elxpi  4523  optocl  4583  fvmptss2  5462  fvmptssdm  5471  acexmidlemcase  5735  elmpocl  5934  mpoxopn0yelv  6102  tfr2a  6184  tfri1dALT  6214  2oconcl  6302  ecexr  6400  ectocld  6461  ecoptocl  6482  eroveu  6486  mapsnconst  6554  diffitest  6747  en2eqpr  6767  ctssdccl  6962  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  dmaddpqlem  7149  nqpi  7150  nq0nn  7214  0nsr  7521  suplocsrlempr  7579  cnm  7604  axaddcl  7636  axmulcl  7638  aprcl  8370  peano2uzs  9328  fzssnn  9788  fzossnn0  9892  rebtwn2zlemstep  9970  fldiv4p1lem1div2  10018  frecfzennn  10139  fser0const  10229  facnn  10413  bcpasc  10452  hashfzo0  10509  rexuz3  10702  rexanuz2  10703  r19.2uz  10705  cau4  10828  caubnd2  10829  climshft2  11015  climaddc1  11038  climmulc2  11040  climsubc1  11041  climsubc2  11042  climlec2  11050  climcau  11056  climcaucn  11060  iserabs  11184  binomlem  11192  isumshft  11199  cvgratgt0  11242  infssuzex  11538  infssuzledc  11539  3prm  11705  phicl2  11785  phibndlem  11787  dfphi2  11791  crth  11795  phimullem  11796  znnen  11806  ennnfonelemkh  11820  bj-el2oss1o  12783  el2oss1o  12990  nninfalllem1  13005  nninfall  13006  isomninnlem  13027
  Copyright terms: Public domain W3C validator