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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811

This theorem is referenced by:  elex2  3419  elex22  3420  disj  4337  disjne  4344  elpr2g  4540  eqoreldif  4575  ordelinel  6270  onun2  6276  ssimaex  6753  fnex  6990  f1ocnv2d  7414  peano5  7624  peano5OLD  7625  mpoexw  7802  tfrlem8  8049  tz7.48-2  8107  tz7.49  8110  eroprf  8426  pssnn  8767  onfin  8789  pssnnOLD  8815  ac6sfi  8836  elfiun  8967  brwdom  9104  ficardom  9463  ficard  10065  tskxpss  10272  inar1  10275  rankcf  10277  tskuni  10283  gruun  10306  nsmallnq  10477  prnmadd  10497  genpss  10504  eqlei  10828  eqlei2  10829  renegcli  11025  supaddc  11685  supadd  11686  supmul1  11687  supmullem2  11689  supmul  11690  nn0ind-raph  12163  uzwo  12393  iccid  12866  hashvnfin  13813  hashdifsnp1  13948  mertenslem2  15333  4sqlem1  16384  4sqlem4  16388  4sqlem11  16391  symggen  18716  psgnran  18761  odlem1  18781  gexlem1  18822  gsumpr  19194  lssvneln0  19842  lss1d  19854  lspsn  19893  lsmelval2  19976  psgnghm  20396  opnneiid  21877  cmpsublem  22150  metrest  23277  metustel  23303  dscopn  23326  ovolshftlem2  24262  subopnmbl  24356  deg1ldgn  24846  plyremlem  25052  coseq0negpitopi  25248  ppiublem1  25938  mptelee  26841  nbuhgr2vtx1edgblem  27293  numclwwlk1lem2foa  28291  shsleji  29305  spansnss  29506  spansncvi  29587  f1o3d  30536  sigaclcu2  31658  measdivcstALTV  31763  dfon2lem6  33338  noextendseq  33513  bdayfo  33523  scutf  33649  altxpsspw  33922  hfun  34123  ontgval  34263  ordtoplem  34267  ordcmp  34279  findreccl  34285  bj-xpnzex  34792  bj-snsetex  34796  bj-ismooredr2  34922  bj-ideqg1  34976  topdifinfindis  35160  finxpreclem1  35203  ovoliunnfl  35462  volsupnfl  35465  heibor1lem  35610  heibor1  35611  lshpkrlem1  36767  lfl1dim  36778  leat3  36952  meetat2  36954  glbconxN  37035  pointpsubN  37408  pmapglbx  37426  linepsubclN  37608  dia2dimlem7  38727  dib1dim2  38825  diclspsn  38851  dih1dimatlem  38986  dihatexv2  38996  djhlsmcl  39071  fsuppssind  39881  fltne  40073  3cubes  40104  hbtlem2  40541  hbtlem5  40545  rp-isfinite6  40699  snssiALTVD  42005  snssiALT  42006  elex2VD  42016  elex22VD  42017  fveqvfvv  44093  afv0fv0  44194  lswn0  44450  lidlmmgm  45037  1neven  45044  cznrng  45067