Theorem eleq1a 2833

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
eleq1a	⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem eleq1a

Step	Hyp	Ref	Expression
1		eleq1 2826	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 250	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  elex2OLD  3502  elex22  3503  disj  4455  disjne  4460  rabsneq  4648  elpr2g  4655  eqoreldif  4689  ordelinel  6486  onun2  6493  ssimaex  6993  fnex  7236  f1ocnv2d  7685  omun  7909  peano5  7915  mpoexw  8101  tfrlem8  8422  tz7.48-2  8480  tz7.49  8483  eroprf  8853  pssnn  9206  onfin  9264  ac6sfi  9317  elfiun  9467  brwdom  9604  ficardom  9998  ficard  10602  tskxpss  10809  inar1  10812  rankcf  10814  tskuni  10820  gruun  10843  nsmallnq  11014  prnmadd  11034  genpss  11041  mpoaddf  11246  mpomulf  11247  eqlei  11368  eqlei2  11369  renegcli  11567  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  supmul  12237  nn0ind-raph  12715  uzwo  12950  iccid  13428  hashvnfin  14395  hashdifsnp1  14541  mertenslem2  15917  4sqlem1  16981  4sqlem4  16985  4sqlem11  16988  symggen  19502  psgnran  19547  odlem1  19567  gexlem1  19611  gsumpr  19987  lssvneln0  20967  lss1d  20978  lspsn  21017  lsmelval2  21101  rnglidlmmgm  21272  psgnghm  21615  opnneiid  23149  cmpsublem  23422  metrest  24552  metustel  24578  dscopn  24601  ovolshftlem2  25558  subopnmbl  25652  deg1ldgn  26146  plyremlem  26360  coseq0negpitopi  26559  ppiublem1  27260  noextendseq  27726  bdayfo  27736  scutf  27871  addsproplem2  28017  mptelee  28924  nbuhgr2vtx1edgblem  29382  numclwwlk1lem2foa  30382  shsleji  31398  spansnss  31599  spansncvi  31680  f1o3d  32643  sigaclcu2  34100  measdivcstALTV  34205  dfon2lem6  35769  altxpsspw  35958  hfun  36159  ontgval  36413  ordtoplem  36417  ordcmp  36429  findreccl  36435  bj-xpnzex  36941  bj-snsetex  36945  bj-ismooredr2  37092  bj-ideqg1  37146  topdifinfindis  37328  finxpreclem1  37371  ovoliunnfl  37648  volsupnfl  37651  heibor1lem  37795  heibor1  37796  lshpkrlem1  39091  lfl1dim  39102  leat3  39276  meetat2  39278  glbconxN  39360  pointpsubN  39733  pmapglbx  39751  linepsubclN  39933  dia2dimlem7  41052  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  dihatexv2  41321  djhlsmcl  41396  fsuppssind  42579  fltne  42630  3cubes  42677  hbtlem2  43112  hbtlem5  43116  rp-isfinite6  43507  snssiALTVD  44824  snssiALT  44825  elex2VD  44835  elex22VD  44836  upwordnul  46833  upwordsing  46837  tworepnotupword  46839  fveqvfvv  46989  afv0fv0  47098  lswn0  47368  1neven  48081  cznrng  48104