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 249	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  elex2OLD  3496  elex22  3497  disj  4448  disjne  4455  elpr2g  4653  eqoreldif  4689  ordelinel  6466  onun2  6473  ssimaex  6977  fnex  7219  f1ocnv2d  7659  omun  7878  peano5  7884  peano5OLD  7885  mpoexw  8065  tfrlem8  8384  tz7.48-2  8442  tz7.49  8445  eroprf  8809  pssnn  9168  onfin  9230  pssnnOLD  9265  ac6sfi  9287  elfiun  9425  brwdom  9562  ficardom  9956  ficard  10560  tskxpss  10767  inar1  10770  rankcf  10772  tskuni  10778  gruun  10801  nsmallnq  10972  prnmadd  10992  genpss  10999  eqlei  11324  eqlei2  11325  renegcli  11521  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  nn0ind-raph  12662  uzwo  12895  iccid  13369  hashvnfin  14320  hashdifsnp1  14457  mertenslem2  15831  4sqlem1  16881  4sqlem4  16885  4sqlem11  16888  symggen  19338  psgnran  19383  odlem1  19403  gexlem1  19447  gsumpr  19823  lssvneln0  20562  lss1d  20574  lspsn  20613  lsmelval2  20696  psgnghm  21133  opnneiid  22630  cmpsublem  22903  metrest  24033  metustel  24059  dscopn  24082  ovolshftlem2  25027  subopnmbl  25121  deg1ldgn  25611  plyremlem  25817  coseq0negpitopi  26013  ppiublem1  26705  noextendseq  27170  bdayfo  27180  scutf  27314  addsproplem2  27456  mptelee  28184  nbuhgr2vtx1edgblem  28639  numclwwlk1lem2foa  29638  shsleji  30654  spansnss  30855  spansncvi  30936  f1o3d  31882  sigaclcu2  33149  measdivcstALTV  33254  dfon2lem6  34791  altxpsspw  34980  hfun  35181  mpomulf  35190  mpoaddf  35216  ontgval  35364  ordtoplem  35368  ordcmp  35380  findreccl  35386  bj-xpnzex  35888  bj-snsetex  35892  bj-ismooredr2  36039  bj-ideqg1  36093  topdifinfindis  36275  finxpreclem1  36318  ovoliunnfl  36578  volsupnfl  36581  heibor1lem  36725  heibor1  36726  lshpkrlem1  38028  lfl1dim  38039  leat3  38213  meetat2  38215  glbconxN  38297  pointpsubN  38670  pmapglbx  38688  linepsubclN  38870  dia2dimlem7  39989  dib1dim2  40087  diclspsn  40113  dih1dimatlem  40248  dihatexv2  40258  djhlsmcl  40333  fsuppssind  41213  fltne  41434  3cubes  41476  hbtlem2  41914  hbtlem5  41918  rp-isfinite6  42317  snssiALTVD  43636  snssiALT  43637  elex2VD  43647  elex22VD  43648  upwordnul  45642  upwordsing  45646  tworepnotupword  45648  fveqvfvv  45798  afv0fv0  45905  lswn0  46160  rnglidlmmgm  46804  1neven  46878  cznrng  46901