Theorem eleq1a 2832

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elex22  3455  disjne  4396  rabsneq  4587  elpr2g  4594  eqoreldif  4630  ordelinel  6420  onun2  6427  ssimaex  6919  fnex  7165  f1ocnv2d  7613  omun  7832  peano5  7837  mpoexw  8024  tfrlem8  8316  tz7.48-2  8374  tz7.49  8377  eroprf  8755  pssnn  9096  onfin  9142  ac6sfi  9187  elfiun  9336  brwdom  9475  ficardom  9876  ficard  10478  tskxpss  10686  inar1  10689  rankcf  10691  tskuni  10697  gruun  10720  nsmallnq  10891  prnmadd  10911  genpss  10918  mpoaddf  11123  mpomulf  11124  eqlei  11247  eqlei2  11248  renegcli  11446  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  supmul  12119  nn0ind-raph  12620  uzwo  12852  iccid  13334  hashvnfin  14313  hashdifsnp1  14459  mertenslem2  15841  4sqlem1  16910  4sqlem4  16914  4sqlem11  16917  symggen  19436  psgnran  19481  odlem1  19501  gexlem1  19545  gsumpr  19921  lssvneln0  20938  lss1d  20949  lspsn  20988  lsmelval2  21072  rnglidlmmgm  21235  psgnghm  21570  opnneiid  23101  cmpsublem  23374  metrest  24499  metustel  24525  dscopn  24548  ovolshftlem2  25487  subopnmbl  25581  deg1ldgn  26068  plyremlem  26281  coseq0negpitopi  26480  ppiublem1  27179  noextendseq  27645  bdayfo  27655  cutsf  27798  addsproplem2  27976  mpteleeOLD  28978  nbuhgr2vtx1edgblem  29434  numclwwlk1lem2foa  30439  shsleji  31456  spansnss  31657  spansncvi  31738  f1o3d  32714  sigaclcu2  34280  measdivcstALTV  34385  dfon2lem6  35984  altxpsspw  36175  hfun  36376  ontgval  36629  ordtoplem  36633  ordcmp  36645  findreccl  36651  bj-xpnzex  37282  bj-snsetex  37286  bj-ismooredr2  37438  bj-ideqg1  37494  topdifinfindis  37676  finxpreclem1  37719  ovoliunnfl  37997  volsupnfl  38000  heibor1lem  38144  heibor1  38145  lshpkrlem1  39570  lfl1dim  39581  leat3  39755  meetat2  39757  glbconxN  39838  pointpsubN  40211  pmapglbx  40229  linepsubclN  40411  dia2dimlem7  41530  dib1dim2  41628  diclspsn  41654  dih1dimatlem  41789  dihatexv2  41799  djhlsmcl  41874  fsuppssind  43040  fltne  43091  3cubes  43136  hbtlem2  43570  hbtlem5  43574  rp-isfinite6  43963  snssiALTVD  45271  snssiALT  45272  elex2VD  45282  elex22VD  45283  fveqvfvv  47500  afv0fv0  47609  lswn0  47916  1neven  48726  cznrng  48749