Theorem eleq2s 2252

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

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  elrabi  2865  opelopabsb  4222  epelg  4252  reg3exmidlemwe  4540  elxpi  4604  optocl  4664  fvmptss2  5545  fvmptssdm  5554  acexmidlemcase  5821  elmpocl  6020  mpoxopn0yelv  6188  tfr2a  6270  tfri1dALT  6300  2oconcl  6388  el2oss1o  6392  ecexr  6487  ectocld  6548  ecoptocl  6569  eroveu  6573  mapsnconst  6641  diffitest  6834  en2eqpr  6854  ctssdccl  7057  exmidonfinlem  7130  exmidfodomrlemr  7139  exmidfodomrlemrALT  7140  dmaddpqlem  7299  nqpi  7300  nq0nn  7364  0nsr  7671  suplocsrlempr  7729  cnm  7754  axaddcl  7786  axmulcl  7788  aprcl  8525  peano2uzs  9500  fzssnn  9976  fzossnn0  10083  rebtwn2zlemstep  10161  fldiv4p1lem1div2  10213  frecfzennn  10334  fser0const  10424  facnn  10612  bcpasc  10651  hashfzo0  10708  rexuz3  10901  rexanuz2  10902  r19.2uz  10904  cau4  11027  caubnd2  11028  climshft2  11214  climaddc1  11237  climmulc2  11239  climsubc1  11240  climsubc2  11241  climlec2  11249  climcau  11255  climcaucn  11259  iserabs  11383  binomlem  11391  isumshft  11398  cvgratgt0  11441  clim2divap  11448  ntrivcvgap  11456  fprodntrivap  11492  fprodeq0  11525  infssuzex  11848  infssuzledc  11849  3prm  12020  phicl2  12104  phibndlem  12106  dfphi2  12110  crth  12114  phimullem  12115  znnen  12197  ennnfonelemkh  12211  bj-el2oss1o  13419  2o01f  13639  nninfalllem1  13651  nninfall  13652