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  4615  ordelinel  6283  ssimaex  6742  fnex  6974  f1ocnv2d  7392  peano5  7599  mpoexw  7770  tfrlem8  8014  tz7.48-2  8072  tz7.49  8075  eroprf  8389  onfin  8703  pssnn  8730  ac6sfi  8756  elfiun  8888  brwdom  9025  ficardom  9384  ficard  9981  tskxpss  10188  inar1  10191  rankcf  10193  tskuni  10199  gruun  10222  nsmallnq  10393  prnmadd  10413  genpss  10420  eqlei  10744  eqlei2  10745  renegcli  10941  supaddc  11602  supadd  11603  supmul1  11604  supmullem2  11606  supmul  11607  nn0ind-raph  12076  uzwo  12305  iccid  12777  hashvnfin  13715  hashdifsnp1  13848  mertenslem2  15235  4sqlem1  16278  4sqlem4  16282  4sqlem11  16285  symggen  18592  psgnran  18637  odlem1  18657  gexlem1  18698  gsumpr  19069  lssvneln0  19717  lss1d  19729  lspsn  19768  lsmelval2  19851  psgnghm  20718  opnneiid  21728  cmpsublem  22001  metrest  23128  metustel  23154  dscopn  23177  ovolshftlem2  24105  subopnmbl  24199  deg1ldgn  24681  plyremlem  24887  coseq0negpitopi  25083  ppiublem1  25772  mptelee  26675  nbuhgr2vtx1edgblem  27127  numclwwlk1lem2foa  28127  shsleji  29141  spansnss  29342  spansncvi  29423  f1o3d  30366  sigaclcu2  31374  measdivcstALTV  31479  dfon2lem6  33028  noextendseq  33169  bdayfo  33177  scutf  33268  altxpsspw  33433  hfun  33634  ontgval  33774  ordtoplem  33778  ordcmp  33790  findreccl  33796  bj-xpnzex  34266  bj-snsetex  34270  bj-ismooredr2  34396  bj-ideqg1  34450  topdifinfindis  34621  finxpreclem1  34664  ovoliunnfl  34928  volsupnfl  34931  heibor1lem  35081  heibor1  35082  lshpkrlem1  36240  lfl1dim  36251  leat3  36425  meetat2  36427  glbconxN  36508  pointpsubN  36881  pmapglbx  36899  linepsubclN  37081  dia2dimlem7  38200  dib1dim2  38298  diclspsn  38324  dih1dimatlem  38459  dihatexv2  38469  djhlsmcl  38544  fltne  39265  3cubes  39280  hbtlem2  39717  hbtlem5  39721  rp-isfinite6  39877  snssiALTVD  41154  snssiALT  41155  elex2VD  41165  elex22VD  41166  fveqvfvv  43269  afv0fv0  43342  lswn0  43598  lidlmmgm  44190  1neven  44197  cznrng  44220