Theorem eleq2s 2325

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

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

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 2212

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-clel 2226

This theorem is referenced by:  elrabi  2958  opelopabsb  4356  epelg  4389  reg3exmidlemwe  4679  elxpi  4743  optocl  4804  elfvm  5675  elfvfvex  5676  fvmbr  5677  fvmptss2  5724  fvmptssdm  5734  acexmidlemcase  6018  elmpocl  6222  mpoxopn0yelv  6410  tfr2a  6492  tfri1dALT  6522  2oconcl  6612  el2oss1o  6616  ecexr  6712  ectocld  6775  ecoptocl  6796  eroveu  6800  mapsnconst  6868  diffitest  7081  en2eqpr  7104  ctssdccl  7315  nninfwlpoimlemginf  7380  exmidonfinlem  7409  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  acnrcl  7421  dmaddpqlem  7602  nqpi  7603  nq0nn  7667  0nsr  7974  suplocsrlempr  8032  cnm  8057  axaddcl  8089  axmulcl  8091  aprcl  8831  aptap  8835  peano2uzs  9823  fzssnn  10308  fzossnn0  10417  infssuzex  10499  infssuzledc  10500  rebtwn2zlemstep  10518  fldiv4p1lem1div2  10571  frecfzennn  10694  fser0const  10803  facnn  10995  bcpasc  11034  hashfzo0  11093  ccatval2  11184  ccatass  11194  pfxclz  11269  wrdeqs1cat  11310  rexuz3  11573  rexanuz2  11574  r19.2uz  11576  cau4  11699  caubnd2  11700  climshft2  11889  climaddc1  11912  climmulc2  11914  climsubc1  11915  climsubc2  11916  climlec2  11924  climcau  11930  climcaucn  11934  iserabs  12059  binomlem  12067  isumshft  12074  cvgratgt0  12117  clim2divap  12124  ntrivcvgap  12132  fprodntrivap  12168  fprodeq0  12201  3prm  12723  phicl2  12809  phibndlem  12811  dfphi2  12815  crth  12819  phimullem  12820  znnen  13042  ennnfonelemkh  13056  fvprif  13449  xpsfeq  13451  ismgmn0  13464  zrhval  14655  lgsdir2lem2  15787  lgsdir2lem3  15788  lgsquadlem2  15836  2lgslem1b  15847  1vgrex  15900  usgredg2v  16104  konigsberglem5  16372  bj-el2oss1o  16431  2o01f  16653  nninfalllem1  16673  nninfall  16674