Theorem eleq2s 2326

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  elrabi  2959  opelopabsb  4354  epelg  4387  reg3exmidlemwe  4677  elxpi  4741  optocl  4802  elfvm  5672  elfvfvex  5673  fvmbr  5674  fvmptss2  5721  fvmptssdm  5731  acexmidlemcase  6013  elmpocl  6217  mpoxopn0yelv  6405  tfr2a  6487  tfri1dALT  6517  2oconcl  6607  el2oss1o  6611  ecexr  6707  ectocld  6770  ecoptocl  6791  eroveu  6795  mapsnconst  6863  diffitest  7076  en2eqpr  7099  ctssdccl  7310  nninfwlpoimlemginf  7375  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  dmaddpqlem  7597  nqpi  7598  nq0nn  7662  0nsr  7969  suplocsrlempr  8027  cnm  8052  axaddcl  8084  axmulcl  8086  aprcl  8826  aptap  8830  peano2uzs  9818  fzssnn  10303  fzossnn0  10412  infssuzex  10494  infssuzledc  10495  rebtwn2zlemstep  10513  fldiv4p1lem1div2  10566  frecfzennn  10689  fser0const  10798  facnn  10990  bcpasc  11029  hashfzo0  11088  ccatval2  11176  ccatass  11186  pfxclz  11261  wrdeqs1cat  11302  rexuz3  11552  rexanuz2  11553  r19.2uz  11555  cau4  11678  caubnd2  11679  climshft2  11868  climaddc1  11891  climmulc2  11893  climsubc1  11894  climsubc2  11895  climlec2  11903  climcau  11909  climcaucn  11913  iserabs  12038  binomlem  12046  isumshft  12053  cvgratgt0  12096  clim2divap  12103  ntrivcvgap  12111  fprodntrivap  12147  fprodeq0  12180  3prm  12702  phicl2  12788  phibndlem  12790  dfphi2  12794  crth  12798  phimullem  12799  znnen  13021  ennnfonelemkh  13035  fvprif  13428  xpsfeq  13430  ismgmn0  13443  zrhval  14634  lgsdir2lem2  15761  lgsdir2lem3  15762  lgsquadlem2  15810  2lgslem1b  15821  1vgrex  15874  usgredg2v  16078  bj-el2oss1o  16391  2o01f  16614  nninfalllem1  16631  nninfall  16632