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 252	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  elex22  3457  disjne  4385  rabsneq  4576  elpr2g  4583  eqoreldif  4619  ordelinel  6416  onun2  6423  ssimaex  6915  fnex  7164  f1ocnv2d  7612  omun  7831  peano5  7837  mpoexw  8022  tfrlem8  8317  tz7.48-2  8375  tz7.49  8378  eroprf  8756  pssnn  9097  onfin  9143  ac6sfi  9188  elfiun  9337  brwdom  9476  ficardom  9880  ficard  10483  tskxpss  10691  inar1  10694  rankcf  10696  tskuni  10702  gruun  10725  nsmallnq  10896  prnmadd  10916  genpss  10923  mpoaddf  11128  mpomulf  11129  eqlei  11252  eqlei2  11253  renegcli  11451  supaddc  12118  supadd  12119  supmul1  12120  supmullem2  12122  supmul  12123  nn0ind-raph  12624  uzwo  12856  iccid  13338  hashvnfin  14317  hashdifsnp1  14463  mertenslem2  15845  4sqlem1  16914  4sqlem4  16918  4sqlem11  16921  symggen  19439  psgnran  19484  odlem1  19504  gexlem1  19548  gsumpr  19924  lssvneln0  20945  lss1d  20956  lspsn  20995  lsmelval2  21078  rnglidlmmgm  21241  psgnghm  21558  opnneiid  23112  cmpsublem  23385  metrest  24510  metustel  24536  dscopn  24559  ovolshftlem2  25498  subopnmbl  25592  deg1ldgn  26079  plyremlem  26291  coseq0negpitopi  26488  ppiublem1  27186  noextendseq  27651  bdayfo  27661  cutsf  27804  addsproplem2  27982  mpteleeOLD  28984  nbuhgr2vtx1edgblem  29440  numclwwlk1lem2foa  30444  shsleji  31461  spansnss  31662  spansncvi  31743  f1o3d  32720  sigaclcu2  34314  measdivcstALTV  34419  dfon2lem6  36027  altxpsspw  36218  hfun  36419  ontgval  36672  ordtoplem  36676  ordcmp  36688  findreccl  36694  bj-xpnzex  37325  bj-snsetex  37329  bj-ismooredr2  37481  bj-ideqg1  37537  topdifinfindis  37721  finxpreclem1  37764  ovoliunnfl  38042  volsupnfl  38045  heibor1lem  38189  heibor1  38190  lshpkrlem1  39615  lfl1dim  39626  leat3  39800  meetat2  39802  glbconxN  39883  pointpsubN  40256  pmapglbx  40274  linepsubclN  40456  dia2dimlem7  41575  dib1dim2  41673  diclspsn  41699  dih1dimatlem  41834  dihatexv2  41844  djhlsmcl  41919  fsuppssind  43056  fltne  43107  3cubes  43152  hbtlem2  43582  hbtlem5  43586  rp-isfinite6  43975  snssiALTVD  45283  snssiALT  45284  elex2VD  45294  elex22VD  45295  fveqvfvv  47515  afv0fv0  47624  lswn0  47931  1neven  48741  cznrng  48764