Theorem eleq2s 2324

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  elrabi  2956  opelopabsb  4349  epelg  4382  reg3exmidlemwe  4672  elxpi  4736  optocl  4797  elfvm  5665  elfvfvex  5666  fvmbr  5667  fvmptss2  5714  fvmptssdm  5724  acexmidlemcase  6005  elmpocl  6209  mpoxopn0yelv  6396  tfr2a  6478  tfri1dALT  6508  2oconcl  6598  el2oss1o  6602  ecexr  6698  ectocld  6761  ecoptocl  6782  eroveu  6786  mapsnconst  6854  diffitest  7062  en2eqpr  7085  ctssdccl  7294  nninfwlpoimlemginf  7359  exmidonfinlem  7387  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  acnrcl  7399  dmaddpqlem  7580  nqpi  7581  nq0nn  7645  0nsr  7952  suplocsrlempr  8010  cnm  8035  axaddcl  8067  axmulcl  8069  aprcl  8809  aptap  8813  peano2uzs  9796  fzssnn  10281  fzossnn0  10390  infssuzex  10470  infssuzledc  10471  rebtwn2zlemstep  10489  fldiv4p1lem1div2  10542  frecfzennn  10665  fser0const  10774  facnn  10966  bcpasc  11005  hashfzo0  11063  ccatval2  11151  ccatass  11161  pfxclz  11232  wrdeqs1cat  11273  rexuz3  11522  rexanuz2  11523  r19.2uz  11525  cau4  11648  caubnd2  11649  climshft2  11838  climaddc1  11861  climmulc2  11863  climsubc1  11864  climsubc2  11865  climlec2  11873  climcau  11879  climcaucn  11883  iserabs  12007  binomlem  12015  isumshft  12022  cvgratgt0  12065  clim2divap  12072  ntrivcvgap  12080  fprodntrivap  12116  fprodeq0  12149  3prm  12671  phicl2  12757  phibndlem  12759  dfphi2  12763  crth  12767  phimullem  12768  znnen  12990  ennnfonelemkh  13004  fvprif  13397  xpsfeq  13399  ismgmn0  13412  zrhval  14602  lgsdir2lem2  15729  lgsdir2lem3  15730  lgsquadlem2  15778  2lgslem1b  15789  1vgrex  15842  usgredg2v  16043  bj-el2oss1o  16247  2o01f  16471  nninfalllem1  16488  nninfall  16489