Theorem eleq2s 2324

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  elrabi  2957  opelopabsb  4352  epelg  4385  reg3exmidlemwe  4675  elxpi  4739  optocl  4800  elfvm  5668  elfvfvex  5669  fvmbr  5670  fvmptss2  5717  fvmptssdm  5727  acexmidlemcase  6008  elmpocl  6212  mpoxopn0yelv  6400  tfr2a  6482  tfri1dALT  6512  2oconcl  6602  el2oss1o  6606  ecexr  6702  ectocld  6765  ecoptocl  6786  eroveu  6790  mapsnconst  6858  diffitest  7071  en2eqpr  7094  ctssdccl  7304  nninfwlpoimlemginf  7369  exmidonfinlem  7397  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  acnrcl  7409  dmaddpqlem  7590  nqpi  7591  nq0nn  7655  0nsr  7962  suplocsrlempr  8020  cnm  8045  axaddcl  8077  axmulcl  8079  aprcl  8819  aptap  8823  peano2uzs  9811  fzssnn  10296  fzossnn0  10405  infssuzex  10486  infssuzledc  10487  rebtwn2zlemstep  10505  fldiv4p1lem1div2  10558  frecfzennn  10681  fser0const  10790  facnn  10982  bcpasc  11021  hashfzo0  11080  ccatval2  11168  ccatass  11178  pfxclz  11253  wrdeqs1cat  11294  rexuz3  11544  rexanuz2  11545  r19.2uz  11547  cau4  11670  caubnd2  11671  climshft2  11860  climaddc1  11883  climmulc2  11885  climsubc1  11886  climsubc2  11887  climlec2  11895  climcau  11901  climcaucn  11905  iserabs  12029  binomlem  12037  isumshft  12044  cvgratgt0  12087  clim2divap  12094  ntrivcvgap  12102  fprodntrivap  12138  fprodeq0  12171  3prm  12693  phicl2  12779  phibndlem  12781  dfphi2  12785  crth  12789  phimullem  12790  znnen  13012  ennnfonelemkh  13026  fvprif  13419  xpsfeq  13421  ismgmn0  13434  zrhval  14624  lgsdir2lem2  15751  lgsdir2lem3  15752  lgsquadlem2  15800  2lgslem1b  15811  1vgrex  15864  usgredg2v  16068  bj-el2oss1o  16320  2o01f  16543  nninfalllem1  16560  nninfall  16561