Theorem eleq1a 2827

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 249	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  elex2OLD  3495  elex22  3496  disj  4447  disjne  4454  elpr2g  4652  eqoreldif  4688  ordelinel  6465  onun2  6472  ssimaex  6976  fnex  7221  f1ocnv2d  7663  omun  7882  peano5  7888  peano5OLD  7889  mpoexw  8069  tfrlem8  8390  tz7.48-2  8448  tz7.49  8451  eroprf  8815  pssnn  9174  onfin  9236  pssnnOLD  9271  ac6sfi  9293  elfiun  9431  brwdom  9568  ficardom  9962  ficard  10566  tskxpss  10773  inar1  10776  rankcf  10778  tskuni  10784  gruun  10807  nsmallnq  10978  prnmadd  10998  genpss  11005  mpomulf  11210  eqlei  11331  eqlei2  11332  renegcli  11528  supaddc  12188  supadd  12189  supmul1  12190  supmullem2  12192  supmul  12193  nn0ind-raph  12669  uzwo  12902  iccid  13376  hashvnfin  14327  hashdifsnp1  14464  mertenslem2  15838  4sqlem1  16888  4sqlem4  16892  4sqlem11  16895  symggen  19386  psgnran  19431  odlem1  19451  gexlem1  19495  gsumpr  19871  lssvneln0  20795  lss1d  20806  lspsn  20845  lsmelval2  20929  rnglidlmmgm  21123  psgnghm  21443  opnneiid  22950  cmpsublem  23223  metrest  24353  metustel  24379  dscopn  24402  ovolshftlem2  25359  subopnmbl  25453  deg1ldgn  25949  plyremlem  26156  coseq0negpitopi  26353  ppiublem1  27048  noextendseq  27513  bdayfo  27523  scutf  27658  addsproplem2  27800  mptelee  28586  nbuhgr2vtx1edgblem  29041  numclwwlk1lem2foa  30040  shsleji  31056  spansnss  31257  spansncvi  31338  f1o3d  32284  sigaclcu2  33582  measdivcstALTV  33687  dfon2lem6  35230  altxpsspw  35419  hfun  35620  mpoaddf  35632  ontgval  35780  ordtoplem  35784  ordcmp  35796  findreccl  35802  bj-xpnzex  36304  bj-snsetex  36308  bj-ismooredr2  36455  bj-ideqg1  36509  topdifinfindis  36691  finxpreclem1  36734  ovoliunnfl  36994  volsupnfl  36997  heibor1lem  37141  heibor1  37142  lshpkrlem1  38444  lfl1dim  38455  leat3  38629  meetat2  38631  glbconxN  38713  pointpsubN  39086  pmapglbx  39104  linepsubclN  39286  dia2dimlem7  40405  dib1dim2  40503  diclspsn  40529  dih1dimatlem  40664  dihatexv2  40674  djhlsmcl  40749  fsuppssind  41628  fltne  41849  3cubes  41891  hbtlem2  42329  hbtlem5  42333  rp-isfinite6  42732  snssiALTVD  44051  snssiALT  44052  elex2VD  44062  elex22VD  44063  upwordnul  46053  upwordsing  46057  tworepnotupword  46059  fveqvfvv  46209  afv0fv0  46316  lswn0  46571  1neven  47075  cznrng  47098