Theorem eleq1a 2824

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806

This theorem is referenced by:  elex2OLD  3492  elex22  3493  disj  4444  disjne  4451  elpr2g  4649  eqoreldif  4685  ordelinel  6465  onun2  6472  ssimaex  6978  fnex  7224  f1ocnv2d  7669  omun  7888  peano5  7894  peano5OLD  7895  mpoexw  8078  tfrlem8  8399  tz7.48-2  8457  tz7.49  8460  eroprf  8828  pssnn  9187  onfin  9249  pssnnOLD  9284  ac6sfi  9306  elfiun  9448  brwdom  9585  ficardom  9979  ficard  10583  tskxpss  10790  inar1  10793  rankcf  10795  tskuni  10801  gruun  10824  nsmallnq  10995  prnmadd  11015  genpss  11022  mpoaddf  11227  mpomulf  11228  eqlei  11349  eqlei2  11350  renegcli  11546  supaddc  12206  supadd  12207  supmul1  12208  supmullem2  12210  supmul  12211  nn0ind-raph  12687  uzwo  12920  iccid  13396  hashvnfin  14346  hashdifsnp1  14484  mertenslem2  15858  4sqlem1  16911  4sqlem4  16915  4sqlem11  16918  symggen  19419  psgnran  19464  odlem1  19484  gexlem1  19528  gsumpr  19904  lssvneln0  20830  lss1d  20841  lspsn  20880  lsmelval2  20964  rnglidlmmgm  21134  psgnghm  21506  opnneiid  23024  cmpsublem  23297  metrest  24427  metustel  24453  dscopn  24476  ovolshftlem2  25433  subopnmbl  25527  deg1ldgn  26023  plyremlem  26233  coseq0negpitopi  26432  ppiublem1  27129  noextendseq  27594  bdayfo  27604  scutf  27739  addsproplem2  27881  mptelee  28700  nbuhgr2vtx1edgblem  29158  numclwwlk1lem2foa  30158  shsleji  31174  spansnss  31375  spansncvi  31456  f1o3d  32406  sigaclcu2  33734  measdivcstALTV  33839  dfon2lem6  35379  altxpsspw  35568  hfun  35769  ontgval  35910  ordtoplem  35914  ordcmp  35926  findreccl  35932  bj-xpnzex  36433  bj-snsetex  36437  bj-ismooredr2  36584  bj-ideqg1  36638  topdifinfindis  36820  finxpreclem1  36863  ovoliunnfl  37130  volsupnfl  37133  heibor1lem  37277  heibor1  37278  lshpkrlem1  38577  lfl1dim  38588  leat3  38762  meetat2  38764  glbconxN  38846  pointpsubN  39219  pmapglbx  39237  linepsubclN  39419  dia2dimlem7  40538  dib1dim2  40636  diclspsn  40662  dih1dimatlem  40797  dihatexv2  40807  djhlsmcl  40882  fsuppssind  41817  fltne  42059  3cubes  42101  hbtlem2  42539  hbtlem5  42543  rp-isfinite6  42939  snssiALTVD  44257  snssiALT  44258  elex2VD  44268  elex22VD  44269  upwordnul  46257  upwordsing  46261  tworepnotupword  46263  fveqvfvv  46413  afv0fv0  46520  lswn0  46775  1neven  47291  cznrng  47314