Theorem eleq2s 2327

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  elrabi  2969  opelopabsb  4377  epelg  4410  reg3exmidlemwe  4700  elxpi  4764  optocl  4825  elfvm  5702  elfvfvex  5703  fvmbr  5704  fvmptss2  5751  fvmptssdm  5761  acexmidlemcase  6044  elmpocl  6248  ressuppss  6453  mpoxopn0yelv  6469  tfr2a  6551  tfri1dALT  6581  2oconcl  6671  el2oss1o  6675  ecexr  6771  ectocld  6834  ecoptocl  6855  eroveu  6859  mapsnconst  6928  diffitest  7143  en2eqpr  7166  ctssdccl  7401  nninfwlpoimlemginf  7466  exmidonfinlem  7495  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  acnrcl  7507  dmaddpqlem  7688  nqpi  7689  nq0nn  7753  0nsr  8060  suplocsrlempr  8118  cnm  8143  axaddcl  8175  axmulcl  8177  aprcl  8916  aptap  8920  peano2uzs  9912  fzssnn  10398  fzossnn0  10507  infssuzex  10589  infssuzledc  10590  rebtwn2zlemstep  10608  fldiv4p1lem1div2  10661  frecfzennn  10784  fser0const  10893  facnn  11085  bcpasc  11124  hashfzo0  11183  hashfibc  11200  ccatval2  11279  ccatass  11289  pfxclz  11364  wrdeqs1cat  11405  rexuz3  11668  rexanuz2  11669  r19.2uz  11671  cau4  11794  caubnd2  11795  climshft2  11984  climaddc1  12007  climmulc2  12009  climsubc1  12010  climsubc2  12011  climlec2  12019  climcau  12025  climcaucn  12029  iserabs  12154  binomlem  12162  isumshft  12169  cvgratgt0  12212  clim2divap  12219  ntrivcvgap  12227  fprodntrivap  12263  fprodeq0  12296  3prm  12818  phicl2  12904  phibndlem  12906  dfphi2  12910  crth  12914  phimullem  12915  znnen  13138  ennnfonelemkh  13152  fvprif  13545  xpsfeq  13547  ismgmn0  13560  zrhval  14752  lgsdir2lem2  15889  lgsdir2lem3  15890  lgsquadlem2  15938  2lgslem1b  15949  1vgrex  16002  usgredg2v  16206  konigsberglem5  16474  bj-el2oss1o  16533  2o01f  16755  nninfalllem1  16773  nninfall  16774