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	|- ( A e. B -> ph )
eleq2s.2	|- C = B

Assertion

Ref	Expression
eleq2s	|- ( A e. C -> ph )

Proof of Theorem eleq2s

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 |- C = B
2	1	eleq2i 2305	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 121	1 |- ( A e. C -> ph )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. 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  6980  diffitest  7195  en2eqpr  7218  ctssdccl  7457  nninfwlpoimlemginf  7522  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acnrcl  7563  dmaddpqlem  7750  nqpi  7751  nq0nn  7815  0nsr  8122  suplocsrlempr  8180  cnm  8205  axaddcl  8237  axmulcl  8239  aprcl  8982  aptap  8986  peano2uzs  10000  fzssnn  10491  fzossnn0  10601  infssuzex  10683  infssuzledc  10684  rebtwn2zlemstep  10704  fldiv4p1lem1div2  10761  frecfzennn  10884  fser0const  10993  facnn  11187  bcpasc  11226  hashfzo0  11286  hashfibc  11305  ccatval2  11388  ccatass  11398  pfxclz  11473  wrdeqs1cat  11514  rexuz3  11778  rexanuz2  11779  r19.2uz  11781  cau4  11905  caubnd2  11906  climshft2  12097  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  climlec2  12132  climcau  12138  climcaucn  12142  iserabs  12267  binomlem  12275  isumshft  12282  cvgratgt0  12325  clim2divap  12332  ntrivcvgap  12340  fprodntrivap  12376  fprodeq0  12409  3prm  12931  phicl2  13021  phibndlem  13023  dfphi2  13027  crth  13031  phimullem  13032  prmlem1a  13250  ballotfilemfmpn  13292  znnen  13347  ennnfonelemkh  13361  ressmex  13478  fvprif  13723  xpsfeq  13725  ismgmn0  13737  cntrval  14151  cntzval  14153  cntzrcl  14159  mgpplusg  14329  mgpbas  14332  ringidval  14372  zrhval  15061  asclfval  15130  gsumbagdiagfi  15176  ppiublem2  16292  lgsdir2lem2  16353  lgsdir2lem3  16354  lgsquadlem2  16402  2lgslem1b  16413  1vgrex  16466  usgredg2v  16670  konigsberglem5  16938  bj-el2oss1o  17007  2o01f  17229  idjudju  17252  nninfalllem1  17257  nninfall  17258