Theorem eleq1a 2858

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  elex22  3479  disjne  4416  rabsneq  4609  elpr2g  4616  eqoreldif  4652  ordelinel  6466  onun2  6473  ssimaex  6968  fnex  7217  f1ocnv2d  7665  omun  7885  peano5  7891  mpoexw  8076  tfrlem8  8372  tz7.48-2  8430  tz7.49  8433  eroprf  8814  pssnn  9154  onfin  9200  ac6sfi  9245  elfiun  9391  brwdom  9530  ficardom  9948  ficard  10550  tskxpss  10758  inar1  10761  rankcf  10763  tskuni  10769  gruun  10792  nsmallnq  10963  prnmadd  10983  genpss  10990  mpoaddf  11195  mpomulf  11196  eqlei  11321  eqlei2  11322  renegcli  11520  supaddc  12183  supadd  12184  supmul1  12185  supmullem2  12187  supmul  12188  nn0ind-raph  12697  uzwo  12936  iccid  13418  hashvnfin  14398  hashdifsnp1  14545  mertenslem2  15941  4sqlem1  17009  4sqlem4  17013  4sqlem11  17016  symggen  19541  psgnran  19586  odlem1  19606  gexlem1  19650  gsumpr  20026  lssvneln0  21054  lss1d  21065  lspsn  21104  lsmelval2  21187  rnglidlmmgm  21360  psgnghm  21711  opnneiid  23264  cmpsublem  23537  metrest  24662  metustel  24688  dscopn  24711  ovolshftlem2  25650  subopnmbl  25744  deg1ldgn  26231  plyremlem  26446  coseq0negpitopi  26649  ppiublem1  27347  noextendseq  27812  bdayfo  27822  cutsf  27966  addsproplem2  28144  mpteleeOLD  29226  nbuhgr2vtx1edgblem  29682  numclwwlk1lem2foa  30686  shsleji  31703  spansnss  31904  spansncvi  31985  f1o3d  32952  sigaclcu2  34491  measdivcstALTV  34596  kardfi  35564  dfon2lem6  36259  altxpsspw  36450  hfun  36651  ontgval  36923  ordtoplem  36927  ordcmp  36939  findreccl  36945  bj-xpnzex  37576  bj-snsetex  37580  bj-ismooredr2  37733  bj-ideqg1  37789  topdifinfindis  37973  finxpreclem1  38016  ovoliunnfl  38294  volsupnfl  38297  heibor1lem  38441  heibor1  38442  lshpkrlem1  39865  lfl1dim  39876  leat3  40050  meetat2  40052  glbconxN  40133  pointpsubN  40506  pmapglbx  40524  linepsubclN  40706  dia2dimlem7  41825  dib1dim2  41923  diclspsn  41949  dih1dimatlem  42084  dihatexv2  42094  djhlsmcl  42169  fsuppssind  43308  fltne  43359  3cubes  43404  hbtlem2  43834  hbtlem5  43838  rp-isfinite6  44227  snssiALTVD  45518  snssiALT  45519  elex2VD  45529  elex22VD  45530  fveqvfvv  47760  afv0fv0  47869  lswn0  48176  1neven  48986  cznrng  49009