Theorem eleq2s 2329

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 2301	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 121	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  elrabi  2972  opelopabsb  4380  epelg  4413  reg3exmidlemwe  4703  elxpi  4767  optocl  4828  elfvm  5705  elfvfvex  5706  fvmbr  5707  fvmptss2  5754  fvmptssdm  5764  acexmidlemcase  6047  elmpocl  6251  ressuppss  6456  mpoxopn0yelv  6472  tfr2a  6554  tfri1dALT  6584  2oconcl  6674  el2oss1o  6678  ecexr  6774  ectocld  6837  ecoptocl  6858  eroveu  6862  mapsnconst  6931  diffitest  7146  en2eqpr  7169  ctssdccl  7404  nninfwlpoimlemginf  7469  exmidonfinlem  7498  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  acnrcl  7510  dmaddpqlem  7697  nqpi  7698  nq0nn  7762  0nsr  8069  suplocsrlempr  8127  cnm  8152  axaddcl  8184  axmulcl  8186  aprcl  8925  aptap  8929  peano2uzs  9922  fzssnn  10408  fzossnn0  10518  infssuzex  10600  infssuzledc  10601  rebtwn2zlemstep  10619  fldiv4p1lem1div2  10672  frecfzennn  10795  fser0const  10904  facnn  11097  bcpasc  11136  hashfzo0  11196  hashfibc  11215  ccatval2  11294  ccatass  11304  pfxclz  11379  wrdeqs1cat  11420  rexuz3  11683  rexanuz2  11684  r19.2uz  11686  cau4  11809  caubnd2  11810  climshft2  11999  climaddc1  12022  climmulc2  12024  climsubc1  12025  climsubc2  12026  climlec2  12034  climcau  12040  climcaucn  12044  iserabs  12169  binomlem  12177  isumshft  12184  cvgratgt0  12227  clim2divap  12234  ntrivcvgap  12242  fprodntrivap  12278  fprodeq0  12311  3prm  12833  phicl2  12919  phibndlem  12921  dfphi2  12925  crth  12929  phimullem  12930  ballotfilemfmpn  13159  znnen  13170  ennnfonelemkh  13184  fvprif  13577  xpsfeq  13579  ismgmn0  13592  zrhval  14814  lgsdir2lem2  15951  lgsdir2lem3  15952  lgsquadlem2  16000  2lgslem1b  16011  1vgrex  16064  usgredg2v  16268  konigsberglem5  16536  bj-el2oss1o  16595  2o01f  16817  nninfalllem1  16835  nninfall  16836