Theorem eleq2s 2182

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

Syntax hints:   → wi 4   = wceq 1289   ∈ wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  elrabi  2768  opelopabsb  4087  epelg  4117  reg3exmidlemwe  4394  elxpi  4454  optocl  4514  fvmptss2  5379  fvmptssdm  5387  acexmidlemcase  5647  elmpt2cl  5842  mpt2xopn0yelv  6004  tfr2a  6086  tfri1dALT  6116  2oconcl  6203  ecexr  6295  ectocld  6356  ecoptocl  6377  eroveu  6381  mapsnconst  6449  diffitest  6601  en2eqpr  6621  exmidfodomrlemr  6826  exmidfodomrlemrALT  6827  dmaddpqlem  6934  nqpi  6935  nq0nn  6999  0nsr  7293  axaddcl  7399  axmulcl  7401  peano2uzs  9070  fzossnn0  9582  rebtwn2zlemstep  9660  fldiv4p1lem1div2  9708  frecfzennn  9829  ser0  9945  fser0const  9947  facnn  10131  bcpasc  10170  hashfzo0  10227  rexuz3  10419  rexanuz2  10420  r19.2uz  10422  cau4  10545  caubnd2  10546  climshft2  10691  climaddc1  10713  climmulc2  10715  climsubc1  10716  climsubc2  10717  climlec2  10726  climcau  10732  climcaucn  10736  iserabs  10865  binomlem  10873  isumshft  10880  cvgratgt0  10923  infssuzex  11219  infssuzledc  11220  3prm  11384  phicl2  11464  phibndlem  11466  dfphi2  11470  crth  11474  phimullem  11475  znnen  11485  el2oss1o  11842  nninfalllem1  11854  nninfall  11855