Theorem eleq2s 2272

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  elrabi  2892  opelopabsb  4262  epelg  4292  reg3exmidlemwe  4580  elxpi  4644  optocl  4704  fvmptss2  5594  fvmptssdm  5603  acexmidlemcase  5873  elmpocl  6072  mpoxopn0yelv  6243  tfr2a  6325  tfri1dALT  6355  2oconcl  6443  el2oss1o  6447  ecexr  6543  ectocld  6604  ecoptocl  6625  eroveu  6629  mapsnconst  6697  diffitest  6890  en2eqpr  6910  ctssdccl  7113  nninfwlpoimlemginf  7177  exmidonfinlem  7195  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  dmaddpqlem  7379  nqpi  7380  nq0nn  7444  0nsr  7751  suplocsrlempr  7809  cnm  7834  axaddcl  7866  axmulcl  7868  aprcl  8606  aptap  8610  peano2uzs  9587  fzssnn  10071  fzossnn0  10178  rebtwn2zlemstep  10256  fldiv4p1lem1div2  10308  frecfzennn  10429  fser0const  10519  facnn  10710  bcpasc  10749  hashfzo0  10806  rexuz3  11002  rexanuz2  11003  r19.2uz  11005  cau4  11128  caubnd2  11129  climshft2  11317  climaddc1  11340  climmulc2  11342  climsubc1  11343  climsubc2  11344  climlec2  11352  climcau  11358  climcaucn  11362  iserabs  11486  binomlem  11494  isumshft  11501  cvgratgt0  11544  clim2divap  11551  ntrivcvgap  11559  fprodntrivap  11595  fprodeq0  11628  infssuzex  11953  infssuzledc  11954  3prm  12131  phicl2  12217  phibndlem  12219  dfphi2  12223  crth  12227  phimullem  12228  znnen  12402  ennnfonelemkh  12416  fvprif  12768  xpsfeq  12770  ismgmn0  12783  lgsdir2lem2  14570  lgsdir2lem3  14571  bj-el2oss1o  14666  2o01f  14887  nninfalllem1  14898  nninfall  14899