Theorem eleq1a 2908

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  elex2  3516  elex22  3517  clel5OLD  3657  disjne  4403  eqoreldif  4621  ordelinel  6288  ssimaex  6747  fnex  6979  f1ocnv2d  7397  peano5  7604  mpoexw  7775  tfrlem8  8019  tz7.48-2  8077  tz7.49  8080  eroprf  8394  onfin  8708  pssnn  8735  ac6sfi  8761  elfiun  8893  brwdom  9030  ficardom  9389  ficard  9986  tskxpss  10193  inar1  10196  rankcf  10198  tskuni  10204  gruun  10227  nsmallnq  10398  prnmadd  10418  genpss  10425  eqlei  10749  eqlei2  10750  renegcli  10946  supaddc  11607  supadd  11608  supmul1  11609  supmullem2  11611  supmul  11612  nn0ind-raph  12081  uzwo  12310  iccid  12782  hashvnfin  13720  hashdifsnp1  13853  mertenslem2  15240  4sqlem1  16283  4sqlem4  16287  4sqlem11  16290  symggen  18597  psgnran  18642  odlem1  18662  gexlem1  18703  gsumpr  19074  lssvneln0  19722  lss1d  19734  lspsn  19773  lsmelval2  19856  psgnghm  20723  opnneiid  21733  cmpsublem  22006  metrest  23133  metustel  23159  dscopn  23182  ovolshftlem2  24110  subopnmbl  24204  deg1ldgn  24686  plyremlem  24892  coseq0negpitopi  25088  ppiublem1  25777  mptelee  26680  nbuhgr2vtx1edgblem  27132  numclwwlk1lem2foa  28132  shsleji  29146  spansnss  29347  spansncvi  29428  f1o3d  30371  sigaclcu2  31379  measdivcstALTV  31484  dfon2lem6  33033  noextendseq  33174  bdayfo  33182  scutf  33273  altxpsspw  33438  hfun  33639  ontgval  33779  ordtoplem  33783  ordcmp  33795  findreccl  33801  bj-xpnzex  34271  bj-snsetex  34275  bj-ismooredr2  34401  bj-ideqg1  34455  topdifinfindis  34626  finxpreclem1  34669  ovoliunnfl  34933  volsupnfl  34936  heibor1lem  35086  heibor1  35087  lshpkrlem1  36245  lfl1dim  36256  leat3  36430  meetat2  36432  glbconxN  36513  pointpsubN  36886  pmapglbx  36904  linepsubclN  37086  dia2dimlem7  38205  dib1dim2  38303  diclspsn  38329  dih1dimatlem  38464  dihatexv2  38474  djhlsmcl  38549  fltne  39270  3cubes  39285  hbtlem2  39722  hbtlem5  39726  rp-isfinite6  39882  snssiALTVD  41159  snssiALT  41160  elex2VD  41170  elex22VD  41171  fveqvfvv  43274  afv0fv0  43347  lswn0  43603  lidlmmgm  44195  1neven  44202  cznrng  44225