Theorem eleq1a 2859

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  elex22  3478  disjne  4411  rabsneq  4603  elpr2g  4610  eqoreldif  4647  ordelinel  6492  onun2  6499  ssimaex  7001  fnex  7254  f1ocnv2d  7706  omun  7933  peano5  7939  mpoexw  8126  tfrlem8  8430  tz7.48-2  8490  tz7.49  8493  eroprf  8874  pssnn  9222  onfin  9268  ac6sfi  9313  elfiun  9459  brwdom  9598  hfunOLD  9956  ficardom  10079  ficard  10688  tskxpss  10896  inar1  10899  rankcf  10901  tskuni  10907  gruun  10930  nsmallnq  11101  prnmadd  11121  genpss  11128  mpoaddf  11333  mpomulf  11334  eqlei  11459  eqlei2  11460  renegcli  11658  supaddc  12324  supadd  12325  supmul1  12326  supmullem2  12328  supmul  12329  nn0ind-raph  12839  uzwo  13078  iccid  13561  hashvnfin  14545  hashdifsnp1  14692  mertenslem2  16098  4sqlem1  17170  4sqlem4  17174  4sqlem11  17177  symggen  19735  psgnran  19780  odlem1  19800  gexlem1  19844  gsumpr  20220  lssvneln0  21278  lss1d  21289  lspsn  21328  lsmelval2  21411  rnglidlmmgm  21584  psgnghm  21941  opnneiid  23499  cmpsublem  23772  metrest  24898  metustel  24924  dscopn  24947  ovolshftlem2  25886  subopnmbl  25980  deg1ldgn  26466  plyremlem  26680  coseq0negpitopi  26889  ppiublem1  27586  fltne  28032  noextendseq  28081  bdayfo  28091  cutsf  28235  addsproplem2  28413  mpteleeOLD  29530  nbuhgr2vtx1edgblem  29989  numclwwlk1lem2foa  31012  shsleji  32029  spansnss  32230  spansncvi  32311  f1o3d  33318  sigaclcu2  34863  measdivcstALTV  34969  kardfi  35979  dfon2lem6  36765  altxpsspw  36957  ontgval  37434  ordtoplem  37438  ordcmp  37450  findreccl  37456  bj-xpnzex  38087  bj-snsetex  38091  bj-ismooredr2  38301  bj-ideqg1  38353  topdifinfindis  38537  finxpreclem1  38580  ovoliunnfl  38848  volsupnfl  38851  heibor1lem  39009  heibor1  39010  lshpkrlem1  40433  lfl1dim  40444  leat3  40618  meetat2  40620  glbconxN  40701  pointpsubN  41074  pmapglbx  41092  linepsubclN  41274  dia2dimlem7  42393  dib1dim2  42491  diclspsn  42517  dih1dimatlem  42652  dihatexv2  42662  djhlsmcl  42737  fsuppssind  43887  3cubes  43966  hbtlem2  44391  hbtlem5  44395  rp-isfinite6  44780  snssiALTVD  46069  snssiALT  46070  elex2VD  46080  elex22VD  46081  mpoexwd  46187  fveqvfvv  48383  afv0fv0  48492  lswn0  48799  1neven  49608  cznrng  49631