Theorem eleq2s 2173

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

Syntax hints:   → wi 4   = wceq 1284   ∈ wcel 1433

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  elrabi  2746  opelopabsb  4015  epelg  4045  reg3exmidlemwe  4321  elxpi  4379  optocl  4434  fvmptss2  5268  fvmptssdm  5276  acexmidlemcase  5527  elmpt2cl  5718  mpt2xopn0yelv  5877  tfr2a  5959  2oconcl  6045  ecexr  6134  ectocld  6195  ecoptocl  6216  eroveu  6220  diffitest  6371  en2eqpr  6380  dmaddpqlem  6567  nqpi  6568  nq0nn  6632  0nsr  6926  axaddcl  7032  axmulcl  7034  peano2uzs  8672  fzossnn0  9184  rebtwn2zlemstep  9261  fldiv4p1lem1div2  9307  frecfzennn  9419  facnn  9654  bcpasc  9693  rexuz3  9876  rexanuz2  9877  r19.2uz  9879  cau4  10002  caubnd2  10003  climshft2  10145  climaddc1  10167  climmulc2  10169  climsubc1  10170  climsubc2  10171  climlec2  10179  climcau  10184  climcaucn  10188  infssuzex  10345  infssuzledc  10346  3prm  10510