Theorem eleq1a 2839

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  elex2OLD  3513  elex22  3514  disj  4473  disjne  4478  rabsneq  4666  elpr2g  4673  eqoreldif  4708  ordelinel  6496  onun2  6503  ssimaex  7007  fnex  7254  f1ocnv2d  7703  omun  7926  peano5  7932  peano5OLD  7933  mpoexw  8119  tfrlem8  8440  tz7.48-2  8498  tz7.49  8501  eroprf  8873  pssnn  9234  onfin  9293  ac6sfi  9348  elfiun  9499  brwdom  9636  ficardom  10030  ficard  10634  tskxpss  10841  inar1  10844  rankcf  10846  tskuni  10852  gruun  10875  nsmallnq  11046  prnmadd  11066  genpss  11073  mpoaddf  11278  mpomulf  11279  eqlei  11400  eqlei2  11401  renegcli  11597  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  nn0ind-raph  12743  uzwo  12976  iccid  13452  hashvnfin  14409  hashdifsnp1  14555  mertenslem2  15933  4sqlem1  16995  4sqlem4  16999  4sqlem11  17002  symggen  19512  psgnran  19557  odlem1  19577  gexlem1  19621  gsumpr  19997  lssvneln0  20973  lss1d  20984  lspsn  21023  lsmelval2  21107  rnglidlmmgm  21278  psgnghm  21621  opnneiid  23155  cmpsublem  23428  metrest  24558  metustel  24584  dscopn  24607  ovolshftlem2  25564  subopnmbl  25658  deg1ldgn  26152  plyremlem  26364  coseq0negpitopi  26563  ppiublem1  27264  noextendseq  27730  bdayfo  27740  scutf  27875  addsproplem2  28021  mptelee  28928  nbuhgr2vtx1edgblem  29386  numclwwlk1lem2foa  30386  shsleji  31402  spansnss  31603  spansncvi  31684  f1o3d  32646  sigaclcu2  34084  measdivcstALTV  34189  dfon2lem6  35752  altxpsspw  35941  hfun  36142  ontgval  36397  ordtoplem  36401  ordcmp  36413  findreccl  36419  bj-xpnzex  36925  bj-snsetex  36929  bj-ismooredr2  37076  bj-ideqg1  37130  topdifinfindis  37312  finxpreclem1  37355  ovoliunnfl  37622  volsupnfl  37625  heibor1lem  37769  heibor1  37770  lshpkrlem1  39066  lfl1dim  39077  leat3  39251  meetat2  39253  glbconxN  39335  pointpsubN  39708  pmapglbx  39726  linepsubclN  39908  dia2dimlem7  41027  dib1dim2  41125  diclspsn  41151  dih1dimatlem  41286  dihatexv2  41296  djhlsmcl  41371  fsuppssind  42548  fltne  42599  3cubes  42646  hbtlem2  43081  hbtlem5  43085  rp-isfinite6  43480  snssiALTVD  44798  snssiALT  44799  elex2VD  44809  elex22VD  44810  upwordnul  46799  upwordsing  46803  tworepnotupword  46805  fveqvfvv  46955  afv0fv0  47064  lswn0  47318  1neven  47961  cznrng  47984