Theorem eleq1a 2835

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

Syntax hints:   → wi 4   = wceq 1539   ∈ 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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  elex2OLD  3454  elex22  3455  disj  4382  disjne  4389  elpr2g  4586  eqoreldif  4621  ordelinel  6368  onun2  6374  ssimaex  6862  fnex  7102  f1ocnv2d  7531  peano5  7749  peano5OLD  7750  mpoexw  7928  tfrlem8  8224  tz7.48-2  8282  tz7.49  8285  eroprf  8613  pssnn  8960  onfin  9022  pssnnOLD  9049  ac6sfi  9067  elfiun  9198  brwdom  9335  ficardom  9728  ficard  10330  tskxpss  10537  inar1  10540  rankcf  10542  tskuni  10548  gruun  10571  nsmallnq  10742  prnmadd  10762  genpss  10769  eqlei  11094  eqlei2  11095  renegcli  11291  supaddc  11951  supadd  11952  supmul1  11953  supmullem2  11955  supmul  11956  nn0ind-raph  12429  uzwo  12660  iccid  13133  hashvnfin  14084  hashdifsnp1  14219  mertenslem2  15606  4sqlem1  16658  4sqlem4  16662  4sqlem11  16665  symggen  19087  psgnran  19132  odlem1  19152  gexlem1  19193  gsumpr  19565  lssvneln0  20222  lss1d  20234  lspsn  20273  lsmelval2  20356  psgnghm  20794  opnneiid  22286  cmpsublem  22559  metrest  23689  metustel  23715  dscopn  23738  ovolshftlem2  24683  subopnmbl  24777  deg1ldgn  25267  plyremlem  25473  coseq0negpitopi  25669  ppiublem1  26359  mptelee  27272  nbuhgr2vtx1edgblem  27727  numclwwlk1lem2foa  28727  shsleji  29741  spansnss  29942  spansncvi  30023  f1o3d  30971  sigaclcu2  32097  measdivcstALTV  32202  dfon2lem6  33773  noextendseq  33879  bdayfo  33889  scutf  34015  altxpsspw  34288  hfun  34489  ontgval  34629  ordtoplem  34633  ordcmp  34645  findreccl  34651  bj-xpnzex  35158  bj-snsetex  35162  bj-ismooredr2  35290  bj-ideqg1  35344  topdifinfindis  35526  finxpreclem1  35569  ovoliunnfl  35828  volsupnfl  35831  heibor1lem  35976  heibor1  35977  lshpkrlem1  37131  lfl1dim  37142  leat3  37316  meetat2  37318  glbconxN  37399  pointpsubN  37772  pmapglbx  37790  linepsubclN  37972  dia2dimlem7  39091  dib1dim2  39189  diclspsn  39215  dih1dimatlem  39350  dihatexv2  39360  djhlsmcl  39435  fsuppssind  40289  fltne  40488  3cubes  40519  hbtlem2  40956  hbtlem5  40960  rp-isfinite6  41132  snssiALTVD  42454  snssiALT  42455  elex2VD  42465  elex22VD  42466  fveqvfvv  44545  afv0fv0  44652  lswn0  44907  lidlmmgm  45494  1neven  45501  cznrng  45524  upwordnul  46526  upwordsing  46530  tworepnotupword  46532