Theorem eleq1a 2831

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 2824	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 250	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elex22  3465  disjne  4407  rabsneq  4599  elpr2g  4606  eqoreldif  4642  ordelinel  6420  onun2  6427  ssimaex  6919  fnex  7163  f1ocnv2d  7611  omun  7830  peano5  7835  mpoexw  8022  tfrlem8  8315  tz7.48-2  8373  tz7.49  8376  eroprf  8752  pssnn  9093  onfin  9139  ac6sfi  9184  elfiun  9333  brwdom  9472  ficardom  9873  ficard  10475  tskxpss  10683  inar1  10686  rankcf  10688  tskuni  10694  gruun  10717  nsmallnq  10888  prnmadd  10908  genpss  10915  mpoaddf  11120  mpomulf  11121  eqlei  11243  eqlei2  11244  renegcli  11442  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  supmul  12114  nn0ind-raph  12592  uzwo  12824  iccid  13306  hashvnfin  14283  hashdifsnp1  14429  mertenslem2  15808  4sqlem1  16876  4sqlem4  16880  4sqlem11  16883  symggen  19399  psgnran  19444  odlem1  19464  gexlem1  19508  gsumpr  19884  lssvneln0  20903  lss1d  20914  lspsn  20953  lsmelval2  21037  rnglidlmmgm  21200  psgnghm  21535  opnneiid  23070  cmpsublem  23343  metrest  24468  metustel  24494  dscopn  24517  ovolshftlem2  25467  subopnmbl  25561  deg1ldgn  26054  plyremlem  26268  coseq0negpitopi  26468  ppiublem1  27169  noextendseq  27635  bdayfo  27645  cutsf  27788  addsproplem2  27966  mpteleeOLD  28968  nbuhgr2vtx1edgblem  29424  numclwwlk1lem2foa  30429  shsleji  31445  spansnss  31646  spansncvi  31727  f1o3d  32704  sigaclcu2  34277  measdivcstALTV  34382  dfon2lem6  35980  altxpsspw  36171  hfun  36372  ontgval  36625  ordtoplem  36629  ordcmp  36641  findreccl  36647  bj-xpnzex  37160  bj-snsetex  37164  bj-ismooredr2  37315  bj-ideqg1  37369  topdifinfindis  37551  finxpreclem1  37594  ovoliunnfl  37863  volsupnfl  37866  heibor1lem  38010  heibor1  38011  lshpkrlem1  39370  lfl1dim  39381  leat3  39555  meetat2  39557  glbconxN  39638  pointpsubN  40011  pmapglbx  40029  linepsubclN  40211  dia2dimlem7  41330  dib1dim2  41428  diclspsn  41454  dih1dimatlem  41589  dihatexv2  41599  djhlsmcl  41674  fsuppssind  42836  fltne  42887  3cubes  42932  hbtlem2  43366  hbtlem5  43370  rp-isfinite6  43759  snssiALTVD  45067  snssiALT  45068  elex2VD  45078  elex22VD  45079  fveqvfvv  47286  afv0fv0  47395  lswn0  47690  1neven  48484  cznrng  48507