Theorem eleq2s 2234

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  elrabi  2837  opelopabsb  4182  epelg  4212  reg3exmidlemwe  4493  elxpi  4555  optocl  4615  fvmptss2  5496  fvmptssdm  5505  acexmidlemcase  5769  elmpocl  5968  mpoxopn0yelv  6136  tfr2a  6218  tfri1dALT  6248  2oconcl  6336  ecexr  6434  ectocld  6495  ecoptocl  6516  eroveu  6520  mapsnconst  6588  diffitest  6781  en2eqpr  6801  ctssdccl  6996  exmidonfinlem  7049  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  dmaddpqlem  7185  nqpi  7186  nq0nn  7250  0nsr  7557  suplocsrlempr  7615  cnm  7640  axaddcl  7672  axmulcl  7674  aprcl  8408  peano2uzs  9379  fzssnn  9848  fzossnn0  9952  rebtwn2zlemstep  10030  fldiv4p1lem1div2  10078  frecfzennn  10199  fser0const  10289  facnn  10473  bcpasc  10512  hashfzo0  10569  rexuz3  10762  rexanuz2  10763  r19.2uz  10765  cau4  10888  caubnd2  10889  climshft2  11075  climaddc1  11098  climmulc2  11100  climsubc1  11101  climsubc2  11102  climlec2  11110  climcau  11116  climcaucn  11120  iserabs  11244  binomlem  11252  isumshft  11259  cvgratgt0  11302  clim2divap  11309  ntrivcvgap  11317  infssuzex  11642  infssuzledc  11643  3prm  11809  phicl2  11890  phibndlem  11892  dfphi2  11896  crth  11900  phimullem  11901  znnen  11911  ennnfonelemkh  11925  bj-el2oss1o  12981  el2oss1o  13188  nninfalllem1  13203  nninfall  13204  isomninnlem  13225