Theorem eleq1a 2828

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

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

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 2115  ax-9 2123  ax-ext 2705

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

This theorem is referenced by:  elex22  3462  disjne  4404  rabsneq  4596  elpr2g  4603  eqoreldif  4639  ordelinel  6416  onun2  6423  ssimaex  6915  fnex  7159  f1ocnv2d  7607  omun  7826  peano5  7831  mpoexw  8018  tfrlem8  8311  tz7.48-2  8369  tz7.49  8372  eroprf  8747  pssnn  9087  onfin  9133  ac6sfi  9177  elfiun  9323  brwdom  9462  ficardom  9863  ficard  10465  tskxpss  10672  inar1  10675  rankcf  10677  tskuni  10683  gruun  10706  nsmallnq  10877  prnmadd  10897  genpss  10904  mpoaddf  11109  mpomulf  11110  eqlei  11232  eqlei2  11233  renegcli  11431  supaddc  12098  supadd  12099  supmul1  12100  supmullem2  12102  supmul  12103  nn0ind-raph  12581  uzwo  12813  iccid  13294  hashvnfin  14271  hashdifsnp1  14417  mertenslem2  15796  4sqlem1  16864  4sqlem4  16868  4sqlem11  16871  symggen  19386  psgnran  19431  odlem1  19451  gexlem1  19495  gsumpr  19871  lssvneln0  20889  lss1d  20900  lspsn  20939  lsmelval2  21023  rnglidlmmgm  21186  psgnghm  21521  opnneiid  23044  cmpsublem  23317  metrest  24442  metustel  24468  dscopn  24491  ovolshftlem2  25441  subopnmbl  25535  deg1ldgn  26028  plyremlem  26242  coseq0negpitopi  26442  ppiublem1  27143  noextendseq  27609  bdayfo  27619  scutf  27756  addsproplem2  27916  mpteleeOLD  28877  nbuhgr2vtx1edgblem  29333  numclwwlk1lem2foa  30338  shsleji  31354  spansnss  31555  spansncvi  31636  f1o3d  32612  sigaclcu2  34156  measdivcstALTV  34261  dfon2lem6  35853  altxpsspw  36044  hfun  36245  ontgval  36498  ordtoplem  36502  ordcmp  36514  findreccl  36520  bj-xpnzex  37026  bj-snsetex  37030  bj-ismooredr2  37177  bj-ideqg1  37231  topdifinfindis  37413  finxpreclem1  37456  ovoliunnfl  37725  volsupnfl  37728  heibor1lem  37872  heibor1  37873  lshpkrlem1  39232  lfl1dim  39243  leat3  39417  meetat2  39419  glbconxN  39500  pointpsubN  39873  pmapglbx  39891  linepsubclN  40073  dia2dimlem7  41192  dib1dim2  41290  diclspsn  41316  dih1dimatlem  41451  dihatexv2  41461  djhlsmcl  41536  fsuppssind  42714  fltne  42765  3cubes  42810  hbtlem2  43244  hbtlem5  43248  rp-isfinite6  43638  snssiALTVD  44946  snssiALT  44947  elex2VD  44957  elex22VD  44958  fveqvfvv  47167  afv0fv0  47276  lswn0  47571  1neven  48365  cznrng  48388