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  4348  epelg  4381  reg3exmidlemwe  4671  elxpi  4735  optocl  4795  elfvm  5662  elfvex  5663  fvmbr  5664  fvmptss2  5711  fvmptssdm  5721  acexmidlemcase  6002  elmpocl  6206  mpoxopn0yelv  6391  tfr2a  6473  tfri1dALT  6503  2oconcl  6593  el2oss1o  6597  ecexr  6693  ectocld  6756  ecoptocl  6777  eroveu  6781  mapsnconst  6849  diffitest  7057  en2eqpr  7077  ctssdccl  7286  nninfwlpoimlemginf  7351  exmidonfinlem  7379  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  acnrcl  7391  dmaddpqlem  7572  nqpi  7573  nq0nn  7637  0nsr  7944  suplocsrlempr  8002  cnm  8027  axaddcl  8059  axmulcl  8061  aprcl  8801  aptap  8805  peano2uzs  9787  fzssnn  10272  fzossnn0  10381  infssuzex  10461  infssuzledc  10462  rebtwn2zlemstep  10480  fldiv4p1lem1div2  10533  frecfzennn  10656  fser0const  10765  facnn  10957  bcpasc  10996  hashfzo0  11053  ccatval2  11141  ccatass  11151  pfxclz  11219  wrdeqs1cat  11260  rexuz3  11509  rexanuz2  11510  r19.2uz  11512  cau4  11635  caubnd2  11636  climshft2  11825  climaddc1  11848  climmulc2  11850  climsubc1  11851  climsubc2  11852  climlec2  11860  climcau  11866  climcaucn  11870  iserabs  11994  binomlem  12002  isumshft  12009  cvgratgt0  12052  clim2divap  12059  ntrivcvgap  12067  fprodntrivap  12103  fprodeq0  12136  3prm  12658  phicl2  12744  phibndlem  12746  dfphi2  12750  crth  12754  phimullem  12755  znnen  12977  ennnfonelemkh  12991  fvprif  13384  xpsfeq  13386  ismgmn0  13399  zrhval  14589  lgsdir2lem2  15716  lgsdir2lem3  15717  lgsquadlem2  15765  2lgslem1b  15776  1vgrex  15829  usgredg2v  16030  bj-el2oss1o  16162  2o01f  16387  nninfalllem1  16404  nninfall  16405