Theorem eleq1a 2826

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  elex22  3461  disjne  4405  rabsneq  4595  elpr2g  4602  eqoreldif  4638  ordelinel  6409  onun2  6416  ssimaex  6907  fnex  7151  f1ocnv2d  7599  omun  7818  peano5  7823  mpoexw  8010  tfrlem8  8303  tz7.48-2  8361  tz7.49  8364  eroprf  8739  pssnn  9078  onfin  9124  ac6sfi  9168  elfiun  9314  brwdom  9453  ficardom  9854  ficard  10456  tskxpss  10663  inar1  10666  rankcf  10668  tskuni  10674  gruun  10697  nsmallnq  10868  prnmadd  10888  genpss  10895  mpoaddf  11100  mpomulf  11101  eqlei  11223  eqlei2  11224  renegcli  11422  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  supmul  12094  nn0ind-raph  12573  uzwo  12809  iccid  13290  hashvnfin  14267  hashdifsnp1  14413  mertenslem2  15792  4sqlem1  16860  4sqlem4  16864  4sqlem11  16867  symggen  19383  psgnran  19428  odlem1  19448  gexlem1  19492  gsumpr  19868  lssvneln0  20886  lss1d  20897  lspsn  20936  lsmelval2  21020  rnglidlmmgm  21183  psgnghm  21518  opnneiid  23042  cmpsublem  23315  metrest  24440  metustel  24466  dscopn  24489  ovolshftlem2  25439  subopnmbl  25533  deg1ldgn  26026  plyremlem  26240  coseq0negpitopi  26440  ppiublem1  27141  noextendseq  27607  bdayfo  27617  scutf  27754  addsproplem2  27914  mptelee  28874  nbuhgr2vtx1edgblem  29330  numclwwlk1lem2foa  30332  shsleji  31348  spansnss  31549  spansncvi  31630  f1o3d  32606  sigaclcu2  34131  measdivcstALTV  34236  dfon2lem6  35828  altxpsspw  36017  hfun  36218  ontgval  36471  ordtoplem  36475  ordcmp  36487  findreccl  36493  bj-xpnzex  36999  bj-snsetex  37003  bj-ismooredr2  37150  bj-ideqg1  37204  topdifinfindis  37386  finxpreclem1  37429  ovoliunnfl  37708  volsupnfl  37711  heibor1lem  37855  heibor1  37856  lshpkrlem1  39155  lfl1dim  39166  leat3  39340  meetat2  39342  glbconxN  39423  pointpsubN  39796  pmapglbx  39814  linepsubclN  39996  dia2dimlem7  41115  dib1dim2  41213  diclspsn  41239  dih1dimatlem  41374  dihatexv2  41384  djhlsmcl  41459  fsuppssind  42632  fltne  42683  3cubes  42729  hbtlem2  43163  hbtlem5  43167  rp-isfinite6  43557  snssiALTVD  44865  snssiALT  44866  elex2VD  44876  elex22VD  44877  fveqvfvv  47077  afv0fv0  47186  lswn0  47481  1neven  48275  cznrng  48298