Theorem eleq2s 2304

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-clel 2205

This theorem is referenced by:  elrabi  2936  opelopabsb  4327  epelg  4358  reg3exmidlemwe  4648  elxpi  4712  optocl  4772  elfvm  5636  fvmptss2  5682  fvmptssdm  5692  acexmidlemcase  5969  elmpocl  6171  mpoxopn0yelv  6355  tfr2a  6437  tfri1dALT  6467  2oconcl  6555  el2oss1o  6559  ecexr  6655  ectocld  6718  ecoptocl  6739  eroveu  6743  mapsnconst  6811  diffitest  7017  en2eqpr  7037  ctssdccl  7246  nninfwlpoimlemginf  7311  exmidonfinlem  7339  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  acnrcl  7351  dmaddpqlem  7532  nqpi  7533  nq0nn  7597  0nsr  7904  suplocsrlempr  7962  cnm  7987  axaddcl  8019  axmulcl  8021  aprcl  8761  aptap  8765  peano2uzs  9747  fzssnn  10232  fzossnn0  10341  infssuzex  10420  infssuzledc  10421  rebtwn2zlemstep  10439  fldiv4p1lem1div2  10492  frecfzennn  10615  fser0const  10724  facnn  10916  bcpasc  10955  hashfzo0  11012  ccatval2  11099  ccatass  11109  pfxclz  11177  wrdeqs1cat  11218  rexuz3  11467  rexanuz2  11468  r19.2uz  11470  cau4  11593  caubnd2  11594  climshft2  11783  climaddc1  11806  climmulc2  11808  climsubc1  11809  climsubc2  11810  climlec2  11818  climcau  11824  climcaucn  11828  iserabs  11952  binomlem  11960  isumshft  11967  cvgratgt0  12010  clim2divap  12017  ntrivcvgap  12025  fprodntrivap  12061  fprodeq0  12094  3prm  12616  phicl2  12702  phibndlem  12704  dfphi2  12708  crth  12712  phimullem  12713  znnen  12935  ennnfonelemkh  12949  fvprif  13342  xpsfeq  13344  ismgmn0  13357  zrhval  14546  lgsdir2lem2  15673  lgsdir2lem3  15674  lgsquadlem2  15722  2lgslem1b  15733  1vgrex  15786  usgredg2v  15987  bj-el2oss1o  16048  2o01f  16269  nninfalllem1  16285  nninfall  16286