Theorem eleq2s 2272

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  elrabi  2890  opelopabsb  4260  epelg  4290  reg3exmidlemwe  4578  elxpi  4642  optocl  4702  fvmptss2  5591  fvmptssdm  5600  acexmidlemcase  5869  elmpocl  6068  mpoxopn0yelv  6239  tfr2a  6321  tfri1dALT  6351  2oconcl  6439  el2oss1o  6443  ecexr  6539  ectocld  6600  ecoptocl  6621  eroveu  6625  mapsnconst  6693  diffitest  6886  en2eqpr  6906  ctssdccl  7109  nninfwlpoimlemginf  7173  exmidonfinlem  7191  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  dmaddpqlem  7375  nqpi  7376  nq0nn  7440  0nsr  7747  suplocsrlempr  7805  cnm  7830  axaddcl  7862  axmulcl  7864  aprcl  8602  aptap  8606  peano2uzs  9583  fzssnn  10067  fzossnn0  10174  rebtwn2zlemstep  10252  fldiv4p1lem1div2  10304  frecfzennn  10425  fser0const  10515  facnn  10706  bcpasc  10745  hashfzo0  10802  rexuz3  10998  rexanuz2  10999  r19.2uz  11001  cau4  11124  caubnd2  11125  climshft2  11313  climaddc1  11336  climmulc2  11338  climsubc1  11339  climsubc2  11340  climlec2  11348  climcau  11354  climcaucn  11358  iserabs  11482  binomlem  11490  isumshft  11497  cvgratgt0  11540  clim2divap  11547  ntrivcvgap  11555  fprodntrivap  11591  fprodeq0  11624  infssuzex  11949  infssuzledc  11950  3prm  12127  phicl2  12213  phibndlem  12215  dfphi2  12219  crth  12223  phimullem  12224  znnen  12398  ennnfonelemkh  12412  fvprif  12761  xpsfeq  12763  ismgmn0  12776  lgsdir2lem2  14400  lgsdir2lem3  14401  bj-el2oss1o  14496  2o01f  14716  nninfalllem1  14727  nninfall  14728