Theorem eleq2s 2288

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  elrabi  2914  opelopabsb  4291  epelg  4322  reg3exmidlemwe  4612  elxpi  4676  optocl  4736  elfvm  5588  fvmptss2  5633  fvmptssdm  5643  acexmidlemcase  5914  elmpocl  6115  mpoxopn0yelv  6294  tfr2a  6376  tfri1dALT  6406  2oconcl  6494  el2oss1o  6498  ecexr  6594  ectocld  6657  ecoptocl  6678  eroveu  6682  mapsnconst  6750  diffitest  6945  en2eqpr  6965  ctssdccl  7172  nninfwlpoimlemginf  7237  exmidonfinlem  7255  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  dmaddpqlem  7439  nqpi  7440  nq0nn  7504  0nsr  7811  suplocsrlempr  7869  cnm  7894  axaddcl  7926  axmulcl  7928  aprcl  8667  aptap  8671  peano2uzs  9652  fzssnn  10137  fzossnn0  10245  rebtwn2zlemstep  10324  fldiv4p1lem1div2  10377  frecfzennn  10500  fser0const  10609  facnn  10801  bcpasc  10840  hashfzo0  10897  rexuz3  11137  rexanuz2  11138  r19.2uz  11140  cau4  11263  caubnd2  11264  climshft2  11452  climaddc1  11475  climmulc2  11477  climsubc1  11478  climsubc2  11479  climlec2  11487  climcau  11493  climcaucn  11497  iserabs  11621  binomlem  11629  isumshft  11636  cvgratgt0  11679  clim2divap  11686  ntrivcvgap  11694  fprodntrivap  11730  fprodeq0  11763  infssuzex  12089  infssuzledc  12090  3prm  12269  phicl2  12355  phibndlem  12357  dfphi2  12361  crth  12365  phimullem  12366  znnen  12558  ennnfonelemkh  12572  fvprif  12929  xpsfeq  12931  ismgmn0  12944  zrhval  14116  lgsdir2lem2  15186  lgsdir2lem3  15187  lgsquadlem2  15235  2lgslem1b  15246  bj-el2oss1o  15336  2o01f  15557  nninfalllem1  15568  nninfall  15569