Theorem eleq1a 2836

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  elex2OLD  3505  elex22  3506  disj  4450  disjne  4455  rabsneq  4644  elpr2g  4651  eqoreldif  4685  ordelinel  6485  onun2  6492  ssimaex  6994  fnex  7237  f1ocnv2d  7686  omun  7909  peano5  7915  mpoexw  8103  tfrlem8  8424  tz7.48-2  8482  tz7.49  8485  eroprf  8855  pssnn  9208  onfin  9267  ac6sfi  9320  elfiun  9470  brwdom  9607  ficardom  10001  ficard  10605  tskxpss  10812  inar1  10815  rankcf  10817  tskuni  10823  gruun  10846  nsmallnq  11017  prnmadd  11037  genpss  11044  mpoaddf  11249  mpomulf  11250  eqlei  11371  eqlei2  11372  renegcli  11570  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  nn0ind-raph  12718  uzwo  12953  iccid  13432  hashvnfin  14399  hashdifsnp1  14545  mertenslem2  15921  4sqlem1  16986  4sqlem4  16990  4sqlem11  16993  symggen  19488  psgnran  19533  odlem1  19553  gexlem1  19597  gsumpr  19973  lssvneln0  20950  lss1d  20961  lspsn  21000  lsmelval2  21084  rnglidlmmgm  21255  psgnghm  21598  opnneiid  23134  cmpsublem  23407  metrest  24537  metustel  24563  dscopn  24586  ovolshftlem2  25545  subopnmbl  25639  deg1ldgn  26132  plyremlem  26346  coseq0negpitopi  26545  ppiublem1  27246  noextendseq  27712  bdayfo  27722  scutf  27857  addsproplem2  28003  mptelee  28910  nbuhgr2vtx1edgblem  29368  numclwwlk1lem2foa  30373  shsleji  31389  spansnss  31590  spansncvi  31671  f1o3d  32637  sigaclcu2  34121  measdivcstALTV  34226  dfon2lem6  35789  altxpsspw  35978  hfun  36179  ontgval  36432  ordtoplem  36436  ordcmp  36448  findreccl  36454  bj-xpnzex  36960  bj-snsetex  36964  bj-ismooredr2  37111  bj-ideqg1  37165  topdifinfindis  37347  finxpreclem1  37390  ovoliunnfl  37669  volsupnfl  37672  heibor1lem  37816  heibor1  37817  lshpkrlem1  39111  lfl1dim  39122  leat3  39296  meetat2  39298  glbconxN  39380  pointpsubN  39753  pmapglbx  39771  linepsubclN  39953  dia2dimlem7  41072  dib1dim2  41170  diclspsn  41196  dih1dimatlem  41331  dihatexv2  41341  djhlsmcl  41416  fsuppssind  42603  fltne  42654  3cubes  42701  hbtlem2  43136  hbtlem5  43140  rp-isfinite6  43531  snssiALTVD  44847  snssiALT  44848  elex2VD  44858  elex22VD  44859  upwordnul  46895  upwordsing  46899  tworepnotupword  46901  fveqvfvv  47052  afv0fv0  47161  lswn0  47431  1neven  48154  cznrng  48177