Theorem eleq1a 2683

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  elex2  3189  elex22  3190  reu6  3362  disjne  3974  eqoreldif  4172  ordelinel  5742  ssimaex  6173  fnex  6386  f1ocnv2d  6784  peano5  6981  tfrlem8  7367  tz7.48-2  7424  tz7.49  7427  eroprf  7732  onfin  8036  pssnn  8063  ac6sfi  8089  elfiun  8219  brwdom  8355  ficardom  8670  ficard  9266  tskxpss  9473  inar1  9476  rankcf  9478  tskuni  9484  gruun  9507  nsmallnq  9678  prnmadd  9698  genpss  9705  eqlei  10026  eqlei2  10027  renegcli  10221  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  nn0ind-raph  11353  uzwo  11627  iccid  12091  hashvnfin  13012  brfi1indlem  13133  mertenslem2  14456  4sqlem1  15490  4sqlem4  15494  4sqlem11  15497  symggen  17713  psgnran  17758  odlem1  17777  gexlem1  17817  lssneln0  18773  lss1d  18784  lspsn  18823  lsmelval2  18906  psgnghm  19745  opnneiid  20740  cmpsublem  21012  metrest  22139  metustel  22165  dscopn  22188  ovolshftlem2  23085  subopnmbl  23178  deg1ldgn  23657  plyremlem  23863  coseq0negpitopi  24059  ppiublem1  24727  mptelee  25575  frgrancvvdeqlem1  26557  frgrawopreglem4  26574  shsleji  27613  spansnss  27814  spansncvi  27895  f1o3d  28813  sigaclcu2  29510  measdivcstOLD  29614  dfon2lem6  30937  bdayfo  31074  altxpsspw  31254  hfun  31455  ontgval  31600  ordtoplem  31604  ordcmp  31616  findreccl  31622  bj-xpnzex  32139  bj-snsetex  32144  topdifinfindis  32370  finxpreclem1  32402  ovoliunnfl  32621  volsupnfl  32624  heibor1lem  32778  heibor1  32779  lshpkrlem1  33415  lfl1dim  33426  leat3  33600  meetat2  33602  glbconxN  33682  pointpsubN  34055  pmapglbx  34073  linepsubclN  34255  dia2dimlem7  35377  dib1dim2  35475  diclspsn  35501  dih1dimatlem  35636  dihatexv2  35646  djhlsmcl  35721  hbtlem2  36713  hbtlem5  36717  rp-isfinite6  36883  snssiALTVD  38084  snssiALT  38085  elex2VD  38095  elex22VD  38096  fveqvfvv  39853  afv0fv0  39878  lswn0  40242  clel5  40303  nbuhgr2vtx1edgblem  40573  frgrncvvdeqlem1  41469  frgrwopreglem4  41484  lidlmmgm  41715  1neven  41722  cznrng  41747  gsumpr  41932