Theorem eleq1a 2829

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  elex2OLD  3484  elex22  3485  disj  4425  disjne  4430  rabsneq  4620  elpr2g  4627  eqoreldif  4661  ordelinel  6455  onun2  6462  ssimaex  6964  fnex  7209  f1ocnv2d  7660  omun  7883  peano5  7889  mpoexw  8077  tfrlem8  8398  tz7.48-2  8456  tz7.49  8459  eroprf  8829  pssnn  9182  onfin  9239  ac6sfi  9292  elfiun  9442  brwdom  9581  ficardom  9975  ficard  10579  tskxpss  10786  inar1  10789  rankcf  10791  tskuni  10797  gruun  10820  nsmallnq  10991  prnmadd  11011  genpss  11018  mpoaddf  11223  mpomulf  11224  eqlei  11345  eqlei2  11346  renegcli  11544  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  nn0ind-raph  12693  uzwo  12927  iccid  13407  hashvnfin  14378  hashdifsnp1  14524  mertenslem2  15901  4sqlem1  16968  4sqlem4  16972  4sqlem11  16975  symggen  19451  psgnran  19496  odlem1  19516  gexlem1  19560  gsumpr  19936  lssvneln0  20909  lss1d  20920  lspsn  20959  lsmelval2  21043  rnglidlmmgm  21206  psgnghm  21540  opnneiid  23064  cmpsublem  23337  metrest  24463  metustel  24489  dscopn  24512  ovolshftlem2  25463  subopnmbl  25557  deg1ldgn  26050  plyremlem  26264  coseq0negpitopi  26464  ppiublem1  27165  noextendseq  27631  bdayfo  27641  scutf  27776  addsproplem2  27929  mptelee  28874  nbuhgr2vtx1edgblem  29330  numclwwlk1lem2foa  30335  shsleji  31351  spansnss  31552  spansncvi  31633  f1o3d  32605  sigaclcu2  34151  measdivcstALTV  34256  dfon2lem6  35806  altxpsspw  35995  hfun  36196  ontgval  36449  ordtoplem  36453  ordcmp  36465  findreccl  36471  bj-xpnzex  36977  bj-snsetex  36981  bj-ismooredr2  37128  bj-ideqg1  37182  topdifinfindis  37364  finxpreclem1  37407  ovoliunnfl  37686  volsupnfl  37689  heibor1lem  37833  heibor1  37834  lshpkrlem1  39128  lfl1dim  39139  leat3  39313  meetat2  39315  glbconxN  39397  pointpsubN  39770  pmapglbx  39788  linepsubclN  39970  dia2dimlem7  41089  dib1dim2  41187  diclspsn  41213  dih1dimatlem  41348  dihatexv2  41358  djhlsmcl  41433  fsuppssind  42616  fltne  42667  3cubes  42713  hbtlem2  43148  hbtlem5  43152  rp-isfinite6  43542  snssiALTVD  44851  snssiALT  44852  elex2VD  44862  elex22VD  44863  upwordnul  46909  upwordsing  46913  tworepnotupword  46915  fveqvfvv  47069  afv0fv0  47178  lswn0  47458  1neven  48213  cznrng  48236