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  2913  opelopabsb  4290  epelg  4321  reg3exmidlemwe  4611  elxpi  4675  optocl  4735  elfvm  5587  fvmptss2  5632  fvmptssdm  5642  acexmidlemcase  5913  elmpocl  6113  mpoxopn0yelv  6292  tfr2a  6374  tfri1dALT  6404  2oconcl  6492  el2oss1o  6496  ecexr  6592  ectocld  6655  ecoptocl  6676  eroveu  6680  mapsnconst  6748  diffitest  6943  en2eqpr  6963  ctssdccl  7170  nninfwlpoimlemginf  7235  exmidonfinlem  7253  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  dmaddpqlem  7437  nqpi  7438  nq0nn  7502  0nsr  7809  suplocsrlempr  7867  cnm  7892  axaddcl  7924  axmulcl  7926  aprcl  8665  aptap  8669  peano2uzs  9649  fzssnn  10134  fzossnn0  10242  rebtwn2zlemstep  10321  fldiv4p1lem1div2  10374  frecfzennn  10497  fser0const  10606  facnn  10798  bcpasc  10837  hashfzo0  10894  rexuz3  11134  rexanuz2  11135  r19.2uz  11137  cau4  11260  caubnd2  11261  climshft2  11449  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  climlec2  11484  climcau  11490  climcaucn  11494  iserabs  11618  binomlem  11626  isumshft  11633  cvgratgt0  11676  clim2divap  11683  ntrivcvgap  11691  fprodntrivap  11727  fprodeq0  11760  infssuzex  12086  infssuzledc  12087  3prm  12266  phicl2  12352  phibndlem  12354  dfphi2  12358  crth  12362  phimullem  12363  znnen  12555  ennnfonelemkh  12569  fvprif  12926  xpsfeq  12928  ismgmn0  12941  zrhval  14105  lgsdir2lem2  15145  lgsdir2lem3  15146  bj-el2oss1o  15266  2o01f  15487  nninfalllem1  15498  nninfall  15499