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  4404  epelg  4437  reg3exmidlemwe  4728  elxpi  4792  optocl  4853  elfvm  5732  elfvfvex  5733  fvmbr  5734  fvmptss2  5783  fvmptssdm  5793  mptmex  5948  acexmidlemcase  6083  elmpocl  6287  ressuppss  6498  mpoxopn0yelv  6514  tfr2a  6596  tfri1dALT  6626  2oconcl  6716  el2oss1o  6720  ecexr  6816  ectocld  6879  ecoptocl  6900  eroveu  6904  mapsnconst  6981  diffitest  7196  en2eqpr  7219  ctssdccl  7458  nninfwlpoimlemginf  7523  exmidonfinlem  7552  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  acnrcl  7564  dmaddpqlem  7751  nqpi  7752  nq0nn  7816  0nsr  8123  suplocsrlempr  8181  cnm  8206  axaddcl  8238  axmulcl  8240  aprcl  8983  aptap  8987  peano2uzs  10001  fzssnn  10492  fzossnn0  10602  infssuzex  10684  infssuzledc  10685  rebtwn2zlemstep  10705  fldiv4p1lem1div2  10762  frecfzennn  10885  fser0const  10994  facnn  11188  bcpasc  11227  hashfzo0  11287  hashfibc  11306  ccatval2  11389  ccatass  11399  pfxclz  11474  wrdeqs1cat  11515  rexuz3  11779  rexanuz2  11780  r19.2uz  11782  cau4  11906  caubnd2  11907  climshft2  12098  climaddc1  12121  climmulc2  12123  climsubc1  12124  climsubc2  12125  climlec2  12133  climcau  12139  climcaucn  12143  iserabs  12268  binomlem  12276  isumshft  12283  cvgratgt0  12326  clim2divap  12333  ntrivcvgap  12341  fprodntrivap  12377  fprodeq0  12410  3prm  12932  phicl2  13022  phibndlem  13024  dfphi2  13028  crth  13032  phimullem  13033  prmlem1a  13251  ballotfilemfmpn  13293  znnen  13348  ennnfonelemkh  13362  ressmex  13479  fvprif  13724  xpsfeq  13726  ismgmn0  13738  cntrval  14152  cntzval  14154  cntzrcl  14160  mgpplusg  14330  mgpbas  14333  ringidval  14373  zrhval  15062  asclfval  15131  gsumbagdiagfi  15181  ppiublem2  16304  lgsdir2lem2  16365  lgsdir2lem3  16366  lgsquadlem2  16414  2lgslem1b  16425  1vgrex  16478  usgredg2v  16682  konigsberglem5  16950  bj-el2oss1o  17019  2o01f  17241  idjudju  17264  nninfalllem1  17269  nninfall  17270