Theorem eleq2s 2132

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

Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  elrabi  2695  opelopabsb  3997  epelg  4027  reg3exmidlemwe  4303  elxpi  4361  optocl  4416  fvmptss2  5247  fvmptssdm  5255  acexmidlemcase  5507  elmpt2cl  5698  mpt2xopn0yelv  5854  tfr2a  5936  2oconcl  6022  ecexr  6111  ectocld  6172  ecoptocl  6193  eroveu  6197  diffitest  6344  dmaddpqlem  6475  nqpi  6476  nq0nn  6540  0nsr  6834  axaddcl  6940  axmulcl  6942  peano2uzs  8527  fzossnn0  9031  rebtwn2zlemstep  9107  fldiv4p1lem1div2  9147  frecfzennn  9203  rexuz3  9588  rexanuz2  9589  r19.2uz  9591  cau4  9712  caubnd2  9713  climshft2  9827  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  climlec2  9861  climcau  9866  climcaucn  9870