Theorem eleq1a 2823

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  elex22  3472  disj  4413  disjne  4418  rabsneq  4608  elpr2g  4615  eqoreldif  4649  ordelinel  6435  onun2  6442  ssimaex  6946  fnex  7191  f1ocnv2d  7642  omun  7864  peano5  7869  mpoexw  8057  tfrlem8  8352  tz7.48-2  8410  tz7.49  8413  eroprf  8788  pssnn  9132  onfin  9179  ac6sfi  9231  elfiun  9381  brwdom  9520  ficardom  9914  ficard  10518  tskxpss  10725  inar1  10728  rankcf  10730  tskuni  10736  gruun  10759  nsmallnq  10930  prnmadd  10950  genpss  10957  mpoaddf  11162  mpomulf  11163  eqlei  11284  eqlei2  11285  renegcli  11483  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  nn0ind-raph  12634  uzwo  12870  iccid  13351  hashvnfin  14325  hashdifsnp1  14471  mertenslem2  15851  4sqlem1  16919  4sqlem4  16923  4sqlem11  16926  symggen  19400  psgnran  19445  odlem1  19465  gexlem1  19509  gsumpr  19885  lssvneln0  20858  lss1d  20869  lspsn  20908  lsmelval2  20992  rnglidlmmgm  21155  psgnghm  21489  opnneiid  23013  cmpsublem  23286  metrest  24412  metustel  24438  dscopn  24461  ovolshftlem2  25411  subopnmbl  25505  deg1ldgn  25998  plyremlem  26212  coseq0negpitopi  26412  ppiublem1  27113  noextendseq  27579  bdayfo  27589  scutf  27724  addsproplem2  27877  mptelee  28822  nbuhgr2vtx1edgblem  29278  numclwwlk1lem2foa  30283  shsleji  31299  spansnss  31500  spansncvi  31581  f1o3d  32551  sigaclcu2  34110  measdivcstALTV  34215  dfon2lem6  35776  altxpsspw  35965  hfun  36166  ontgval  36419  ordtoplem  36423  ordcmp  36435  findreccl  36441  bj-xpnzex  36947  bj-snsetex  36951  bj-ismooredr2  37098  bj-ideqg1  37152  topdifinfindis  37334  finxpreclem1  37377  ovoliunnfl  37656  volsupnfl  37659  heibor1lem  37803  heibor1  37804  lshpkrlem1  39103  lfl1dim  39114  leat3  39288  meetat2  39290  glbconxN  39372  pointpsubN  39745  pmapglbx  39763  linepsubclN  39945  dia2dimlem7  41064  dib1dim2  41162  diclspsn  41188  dih1dimatlem  41323  dihatexv2  41333  djhlsmcl  41408  fsuppssind  42581  fltne  42632  3cubes  42678  hbtlem2  43113  hbtlem5  43117  rp-isfinite6  43507  snssiALTVD  44816  snssiALT  44817  elex2VD  44827  elex22VD  44828  upwordnul  46878  upwordsing  46882  tworepnotupword  46884  fveqvfvv  47041  afv0fv0  47150  lswn0  47445  1neven  48226  cznrng  48249