Theorem eleq2s 2333

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  elrabi  2979  opelopabsb  4402  epelg  4435  reg3exmidlemwe  4726  elxpi  4790  optocl  4851  elfvm  5729  elfvfvex  5730  fvmbr  5731  fvmptss2  5780  fvmptssdm  5790  mptmex  5945  acexmidlemcase  6080  elmpocl  6284  ressuppss  6494  mpoxopn0yelv  6510  tfr2a  6592  tfri1dALT  6622  2oconcl  6712  el2oss1o  6716  ecexr  6812  ectocld  6875  ecoptocl  6896  eroveu  6900  mapsnconst  6976  diffitest  7191  en2eqpr  7214  ctssdccl  7451  nninfwlpoimlemginf  7516  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnrcl  7557  dmaddpqlem  7744  nqpi  7745  nq0nn  7809  0nsr  8116  suplocsrlempr  8174  cnm  8199  axaddcl  8231  axmulcl  8233  aprcl  8975  aptap  8979  peano2uzs  9986  fzssnn  10476  fzossnn0  10586  infssuzex  10668  infssuzledc  10669  rebtwn2zlemstep  10689  fldiv4p1lem1div2  10742  frecfzennn  10865  fser0const  10974  facnn  11167  bcpasc  11206  hashfzo0  11266  hashfibc  11285  ccatval2  11368  ccatass  11378  pfxclz  11453  wrdeqs1cat  11494  rexuz3  11758  rexanuz2  11759  r19.2uz  11761  cau4  11884  caubnd2  11885  climshft2  12074  climaddc1  12097  climmulc2  12099  climsubc1  12100  climsubc2  12101  climlec2  12109  climcau  12115  climcaucn  12119  iserabs  12244  binomlem  12252  isumshft  12259  cvgratgt0  12302  clim2divap  12309  ntrivcvgap  12317  fprodntrivap  12353  fprodeq0  12386  3prm  12908  phicl2  12994  phibndlem  12996  dfphi2  13000  crth  13004  phimullem  13005  ballotfilemfmpn  13236  znnen  13291  ennnfonelemkh  13305  fvprif  13666  xpsfeq  13668  ismgmn0  13680  mgpplusg  14224  mgpbas  14227  ringidval  14267  zrhval  14954  asclfval  15023  lgsdir2lem2  16160  lgsdir2lem3  16161  lgsquadlem2  16209  2lgslem1b  16220  1vgrex  16273  usgredg2v  16477  konigsberglem5  16745  bj-el2oss1o  16814  2o01f  17036  nninfalllem1  17063  nninfall  17064