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  2892  opelopabsb  4262  epelg  4292  reg3exmidlemwe  4580  elxpi  4644  optocl  4704  fvmptss2  5593  fvmptssdm  5602  acexmidlemcase  5872  elmpocl  6071  mpoxopn0yelv  6242  tfr2a  6324  tfri1dALT  6354  2oconcl  6442  el2oss1o  6446  ecexr  6542  ectocld  6603  ecoptocl  6624  eroveu  6628  mapsnconst  6696  diffitest  6889  en2eqpr  6909  ctssdccl  7112  nninfwlpoimlemginf  7176  exmidonfinlem  7194  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  dmaddpqlem  7378  nqpi  7379  nq0nn  7443  0nsr  7750  suplocsrlempr  7808  cnm  7833  axaddcl  7865  axmulcl  7867  aprcl  8605  aptap  8609  peano2uzs  9586  fzssnn  10070  fzossnn0  10177  rebtwn2zlemstep  10255  fldiv4p1lem1div2  10307  frecfzennn  10428  fser0const  10518  facnn  10709  bcpasc  10748  hashfzo0  10805  rexuz3  11001  rexanuz2  11002  r19.2uz  11004  cau4  11127  caubnd2  11128  climshft2  11316  climaddc1  11339  climmulc2  11341  climsubc1  11342  climsubc2  11343  climlec2  11351  climcau  11357  climcaucn  11361  iserabs  11485  binomlem  11493  isumshft  11500  cvgratgt0  11543  clim2divap  11550  ntrivcvgap  11558  fprodntrivap  11594  fprodeq0  11627  infssuzex  11952  infssuzledc  11953  3prm  12130  phicl2  12216  phibndlem  12218  dfphi2  12222  crth  12226  phimullem  12227  znnen  12401  ennnfonelemkh  12415  fvprif  12767  xpsfeq  12769  ismgmn0  12782  lgsdir2lem2  14469  lgsdir2lem3  14470  bj-el2oss1o  14565  2o01f  14785  nninfalllem1  14796  nninfall  14797