Theorem eleq1a 2835

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815

This theorem is referenced by:  elex22  3457  disjne  4390  rabsneq  4581  elpr2g  4588  eqoreldif  4624  ordelinel  6420  onun2  6427  ssimaex  6919  fnex  7168  f1ocnv2d  7616  omun  7835  peano5  7840  mpoexw  8027  tfrlem8  8320  tz7.48-2  8378  tz7.49  8381  eroprf  8759  pssnn  9100  onfin  9146  ac6sfi  9191  elfiun  9340  brwdom  9479  ficardom  9883  ficard  10485  tskxpss  10693  inar1  10696  rankcf  10698  tskuni  10704  gruun  10727  nsmallnq  10898  prnmadd  10918  genpss  10925  mpoaddf  11130  mpomulf  11131  eqlei  11254  eqlei2  11255  renegcli  11453  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  nn0ind-raph  12627  uzwo  12859  iccid  13341  hashvnfin  14320  hashdifsnp1  14466  mertenslem2  15848  4sqlem1  16917  4sqlem4  16921  4sqlem11  16924  symggen  19443  psgnran  19488  odlem1  19508  gexlem1  19552  gsumpr  19928  lssvneln0  20949  lss1d  20960  lspsn  20999  lsmelval2  21082  rnglidlmmgm  21245  psgnghm  21562  opnneiid  23116  cmpsublem  23389  metrest  24514  metustel  24540  dscopn  24563  ovolshftlem2  25502  subopnmbl  25596  deg1ldgn  26083  plyremlem  26295  coseq0negpitopi  26492  ppiublem1  27190  noextendseq  27656  bdayfo  27666  cutsf  27809  addsproplem2  27987  mpteleeOLD  28989  nbuhgr2vtx1edgblem  29445  numclwwlk1lem2foa  30449  shsleji  31466  spansnss  31667  spansncvi  31748  f1o3d  32725  sigaclcu2  34311  measdivcstALTV  34416  dfon2lem6  36021  altxpsspw  36212  hfun  36413  ontgval  36666  ordtoplem  36670  ordcmp  36682  findreccl  36688  bj-xpnzex  37319  bj-snsetex  37323  bj-ismooredr2  37475  bj-ideqg1  37531  topdifinfindis  37715  finxpreclem1  37758  ovoliunnfl  38036  volsupnfl  38039  heibor1lem  38183  heibor1  38184  lshpkrlem1  39609  lfl1dim  39620  leat3  39794  meetat2  39796  glbconxN  39877  pointpsubN  40250  pmapglbx  40268  linepsubclN  40450  dia2dimlem7  41569  dib1dim2  41667  diclspsn  41693  dih1dimatlem  41828  dihatexv2  41838  djhlsmcl  41913  fsuppssind  43050  fltne  43101  3cubes  43146  hbtlem2  43576  hbtlem5  43580  rp-isfinite6  43969  snssiALTVD  45277  snssiALT  45278  elex2VD  45288  elex22VD  45289  fveqvfvv  47510  afv0fv0  47619  lswn0  47926  1neven  48736  cznrng  48759