Theorem eleq2s 2291

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

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 ⊢ 𝐶 = 𝐵
2	1	eleq2i 2263	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 121	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  elrabi  2917  opelopabsb  4295  epelg  4326  reg3exmidlemwe  4616  elxpi  4680  optocl  4740  elfvm  5592  fvmptss2  5637  fvmptssdm  5647  acexmidlemcase  5918  elmpocl  6119  mpoxopn0yelv  6298  tfr2a  6380  tfri1dALT  6410  2oconcl  6498  el2oss1o  6502  ecexr  6598  ectocld  6661  ecoptocl  6682  eroveu  6686  mapsnconst  6754  diffitest  6949  en2eqpr  6969  ctssdccl  7178  nninfwlpoimlemginf  7243  exmidonfinlem  7262  exmidfodomrlemr  7271  exmidfodomrlemrALT  7272  dmaddpqlem  7446  nqpi  7447  nq0nn  7511  0nsr  7818  suplocsrlempr  7876  cnm  7901  axaddcl  7933  axmulcl  7935  aprcl  8675  aptap  8679  peano2uzs  9660  fzssnn  10145  fzossnn0  10253  infssuzex  10325  infssuzledc  10326  rebtwn2zlemstep  10344  fldiv4p1lem1div2  10397  frecfzennn  10520  fser0const  10629  facnn  10821  bcpasc  10860  hashfzo0  10917  rexuz3  11157  rexanuz2  11158  r19.2uz  11160  cau4  11283  caubnd2  11284  climshft2  11473  climaddc1  11496  climmulc2  11498  climsubc1  11499  climsubc2  11500  climlec2  11508  climcau  11514  climcaucn  11518  iserabs  11642  binomlem  11650  isumshft  11657  cvgratgt0  11700  clim2divap  11707  ntrivcvgap  11715  fprodntrivap  11751  fprodeq0  11784  3prm  12306  phicl2  12392  phibndlem  12394  dfphi2  12398  crth  12402  phimullem  12403  znnen  12625  ennnfonelemkh  12639  fvprif  12996  xpsfeq  12998  ismgmn0  13011  zrhval  14183  lgsdir2lem2  15280  lgsdir2lem3  15281  lgsquadlem2  15329  2lgslem1b  15340  bj-el2oss1o  15430  2o01f  15651  nninfalllem1  15662  nninfall  15663