Theorem eleq1a 2826

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  elex22  3461  disjne  4402  rabsneq  4592  elpr2g  4599  eqoreldif  4635  ordelinel  6409  onun2  6416  ssimaex  6907  fnex  7151  f1ocnv2d  7599  omun  7818  peano5  7823  mpoexw  8010  tfrlem8  8303  tz7.48-2  8361  tz7.49  8364  eroprf  8739  pssnn  9078  onfin  9124  ac6sfi  9168  elfiun  9314  brwdom  9453  ficardom  9854  ficard  10456  tskxpss  10663  inar1  10666  rankcf  10668  tskuni  10674  gruun  10697  nsmallnq  10868  prnmadd  10888  genpss  10895  mpoaddf  11100  mpomulf  11101  eqlei  11223  eqlei2  11224  renegcli  11422  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  supmul  12094  nn0ind-raph  12573  uzwo  12809  iccid  13290  hashvnfin  14267  hashdifsnp1  14413  mertenslem2  15792  4sqlem1  16860  4sqlem4  16864  4sqlem11  16867  symggen  19382  psgnran  19427  odlem1  19447  gexlem1  19491  gsumpr  19867  lssvneln0  20885  lss1d  20896  lspsn  20935  lsmelval2  21019  rnglidlmmgm  21182  psgnghm  21517  opnneiid  23041  cmpsublem  23314  metrest  24439  metustel  24465  dscopn  24488  ovolshftlem2  25438  subopnmbl  25532  deg1ldgn  26025  plyremlem  26239  coseq0negpitopi  26439  ppiublem1  27140  noextendseq  27606  bdayfo  27616  scutf  27753  addsproplem2  27913  mptelee  28873  nbuhgr2vtx1edgblem  29329  numclwwlk1lem2foa  30334  shsleji  31350  spansnss  31551  spansncvi  31632  f1o3d  32608  sigaclcu2  34133  measdivcstALTV  34238  dfon2lem6  35830  altxpsspw  36021  hfun  36222  ontgval  36475  ordtoplem  36479  ordcmp  36491  findreccl  36497  bj-xpnzex  37003  bj-snsetex  37007  bj-ismooredr2  37154  bj-ideqg1  37208  topdifinfindis  37390  finxpreclem1  37433  ovoliunnfl  37701  volsupnfl  37704  heibor1lem  37848  heibor1  37849  lshpkrlem1  39208  lfl1dim  39219  leat3  39393  meetat2  39395  glbconxN  39476  pointpsubN  39849  pmapglbx  39867  linepsubclN  40049  dia2dimlem7  41168  dib1dim2  41266  diclspsn  41292  dih1dimatlem  41427  dihatexv2  41437  djhlsmcl  41512  fsuppssind  42685  fltne  42736  3cubes  42782  hbtlem2  43216  hbtlem5  43220  rp-isfinite6  43610  snssiALTVD  44918  snssiALT  44919  elex2VD  44929  elex22VD  44930  fveqvfvv  47139  afv0fv0  47248  lswn0  47543  1neven  48337  cznrng  48360