Theorem eleq2s 2235

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  elrabi  2841  opelopabsb  4190  epelg  4220  reg3exmidlemwe  4501  elxpi  4563  optocl  4623  fvmptss2  5504  fvmptssdm  5513  acexmidlemcase  5777  elmpocl  5976  mpoxopn0yelv  6144  tfr2a  6226  tfri1dALT  6256  2oconcl  6344  ecexr  6442  ectocld  6503  ecoptocl  6524  eroveu  6528  mapsnconst  6596  diffitest  6789  en2eqpr  6809  ctssdccl  7004  exmidonfinlem  7066  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  dmaddpqlem  7209  nqpi  7210  nq0nn  7274  0nsr  7581  suplocsrlempr  7639  cnm  7664  axaddcl  7696  axmulcl  7698  aprcl  8432  peano2uzs  9406  fzssnn  9879  fzossnn0  9983  rebtwn2zlemstep  10061  fldiv4p1lem1div2  10109  frecfzennn  10230  fser0const  10320  facnn  10505  bcpasc  10544  hashfzo0  10601  rexuz3  10794  rexanuz2  10795  r19.2uz  10797  cau4  10920  caubnd2  10921  climshft2  11107  climaddc1  11130  climmulc2  11132  climsubc1  11133  climsubc2  11134  climlec2  11142  climcau  11148  climcaucn  11152  iserabs  11276  binomlem  11284  isumshft  11291  cvgratgt0  11334  clim2divap  11341  ntrivcvgap  11349  infssuzex  11678  infssuzledc  11679  3prm  11845  phicl2  11926  phibndlem  11928  dfphi2  11932  crth  11936  phimullem  11937  znnen  11947  ennnfonelemkh  11961  bj-el2oss1o  13152  el2oss1o  13359  2o01f  13364  nninfalllem1  13378  nninfall  13379