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  3463  disj  4403  disjne  4408  rabsneq  4598  elpr2g  4605  eqoreldif  4639  ordelinel  6414  onun2  6421  ssimaex  6912  fnex  7157  f1ocnv2d  7606  omun  7828  peano5  7833  mpoexw  8020  tfrlem8  8313  tz7.48-2  8371  tz7.49  8374  eroprf  8749  pssnn  9092  onfin  9139  ac6sfi  9189  elfiun  9339  brwdom  9478  ficardom  9876  ficard  10478  tskxpss  10685  inar1  10688  rankcf  10690  tskuni  10696  gruun  10719  nsmallnq  10890  prnmadd  10910  genpss  10917  mpoaddf  11122  mpomulf  11123  eqlei  11244  eqlei2  11245  renegcli  11443  supaddc  12110  supadd  12111  supmul1  12112  supmullem2  12114  supmul  12115  nn0ind-raph  12594  uzwo  12830  iccid  13311  hashvnfin  14285  hashdifsnp1  14431  mertenslem2  15810  4sqlem1  16878  4sqlem4  16882  4sqlem11  16885  symggen  19367  psgnran  19412  odlem1  19432  gexlem1  19476  gsumpr  19852  lssvneln0  20873  lss1d  20884  lspsn  20923  lsmelval2  21007  rnglidlmmgm  21170  psgnghm  21505  opnneiid  23029  cmpsublem  23302  metrest  24428  metustel  24454  dscopn  24477  ovolshftlem2  25427  subopnmbl  25521  deg1ldgn  26014  plyremlem  26228  coseq0negpitopi  26428  ppiublem1  27129  noextendseq  27595  bdayfo  27605  scutf  27741  addsproplem2  27900  mptelee  28858  nbuhgr2vtx1edgblem  29314  numclwwlk1lem2foa  30316  shsleji  31332  spansnss  31533  spansncvi  31614  f1o3d  32584  sigaclcu2  34089  measdivcstALTV  34194  dfon2lem6  35764  altxpsspw  35953  hfun  36154  ontgval  36407  ordtoplem  36411  ordcmp  36423  findreccl  36429  bj-xpnzex  36935  bj-snsetex  36939  bj-ismooredr2  37086  bj-ideqg1  37140  topdifinfindis  37322  finxpreclem1  37365  ovoliunnfl  37644  volsupnfl  37647  heibor1lem  37791  heibor1  37792  lshpkrlem1  39091  lfl1dim  39102  leat3  39276  meetat2  39278  glbconxN  39360  pointpsubN  39733  pmapglbx  39751  linepsubclN  39933  dia2dimlem7  41052  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  dihatexv2  41321  djhlsmcl  41396  fsuppssind  42569  fltne  42620  3cubes  42666  hbtlem2  43100  hbtlem5  43104  rp-isfinite6  43494  snssiALTVD  44803  snssiALT  44804  elex2VD  44814  elex22VD  44815  upwordnul  46865  upwordsing  46869  tworepnotupword  46871  fveqvfvv  47028  afv0fv0  47137  lswn0  47432  1neven  48226  cznrng  48249