Theorem eleq1a 2860

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840

This theorem is referenced by:  elex22  3481  disjne  4412  rabsneq  4604  elpr2g  4611  eqoreldif  4647  ordelinel  6453  onun2  6460  ssimaex  6956  fnex  7205  f1ocnv2d  7653  omun  7872  peano5  7878  mpoexw  8063  tfrlem8  8359  tz7.48-2  8417  tz7.49  8420  eroprf  8801  pssnn  9141  onfin  9187  ac6sfi  9232  elfiun  9378  brwdom  9517  ficardom  9935  ficard  10537  tskxpss  10745  inar1  10748  rankcf  10750  tskuni  10756  gruun  10779  nsmallnq  10950  prnmadd  10970  genpss  10977  mpoaddf  11182  mpomulf  11183  eqlei  11308  eqlei2  11309  renegcli  11507  supaddc  12170  supadd  12171  supmul1  12172  supmullem2  12174  supmul  12175  nn0ind-raph  12684  uzwo  12923  iccid  13405  hashvnfin  14384  hashdifsnp1  14531  mertenslem2  15927  4sqlem1  16996  4sqlem4  17000  4sqlem11  17003  symggen  19528  psgnran  19573  odlem1  19593  gexlem1  19637  gsumpr  20013  lssvneln0  21039  lss1d  21050  lspsn  21089  lsmelval2  21172  rnglidlmmgm  21341  psgnghm  21687  opnneiid  23240  cmpsublem  23513  metrest  24638  metustel  24664  dscopn  24687  ovolshftlem2  25626  subopnmbl  25720  deg1ldgn  26207  plyremlem  26422  coseq0negpitopi  26622  ppiublem1  27320  noextendseq  27785  bdayfo  27795  cutsf  27939  addsproplem2  28117  mpteleeOLD  29150  nbuhgr2vtx1edgblem  29606  numclwwlk1lem2foa  30610  shsleji  31627  spansnss  31828  spansncvi  31909  f1o3d  32879  sigaclcu2  34422  measdivcstALTV  34527  dfon2lem6  36144  altxpsspw  36335  hfun  36536  ontgval  36799  ordtoplem  36803  ordcmp  36815  findreccl  36821  bj-xpnzex  37451  bj-snsetex  37455  bj-ismooredr2  37607  bj-ideqg1  37663  topdifinfindis  37847  finxpreclem1  37890  ovoliunnfl  38168  volsupnfl  38171  heibor1lem  38315  heibor1  38316  lshpkrlem1  39741  lfl1dim  39752  leat3  39926  meetat2  39928  glbconxN  40009  pointpsubN  40382  pmapglbx  40400  linepsubclN  40582  dia2dimlem7  41701  dib1dim2  41799  diclspsn  41825  dih1dimatlem  41960  dihatexv2  41970  djhlsmcl  42045  fsuppssind  43182  fltne  43233  3cubes  43278  hbtlem2  43708  hbtlem5  43712  rp-isfinite6  44101  snssiALTVD  45394  snssiALT  45395  elex2VD  45405  elex22VD  45406  fveqvfvv  47633  afv0fv0  47742  lswn0  48049  1neven  48859  cznrng  48882