Theorem eleq1a 2832

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elex22  3467  disjne  4409  rabsneq  4601  elpr2g  4608  eqoreldif  4644  ordelinel  6428  onun2  6435  ssimaex  6927  fnex  7173  f1ocnv2d  7621  omun  7840  peano5  7845  mpoexw  8032  tfrlem8  8325  tz7.48-2  8383  tz7.49  8386  eroprf  8764  pssnn  9105  onfin  9151  ac6sfi  9196  elfiun  9345  brwdom  9484  ficardom  9885  ficard  10487  tskxpss  10695  inar1  10698  rankcf  10700  tskuni  10706  gruun  10729  nsmallnq  10900  prnmadd  10920  genpss  10927  mpoaddf  11132  mpomulf  11133  eqlei  11255  eqlei2  11256  renegcli  11454  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  nn0ind-raph  12604  uzwo  12836  iccid  13318  hashvnfin  14295  hashdifsnp1  14441  mertenslem2  15820  4sqlem1  16888  4sqlem4  16892  4sqlem11  16895  symggen  19411  psgnran  19456  odlem1  19476  gexlem1  19520  gsumpr  19896  lssvneln0  20915  lss1d  20926  lspsn  20965  lsmelval2  21049  rnglidlmmgm  21212  psgnghm  21547  opnneiid  23082  cmpsublem  23355  metrest  24480  metustel  24506  dscopn  24529  ovolshftlem2  25479  subopnmbl  25573  deg1ldgn  26066  plyremlem  26280  coseq0negpitopi  26480  ppiublem1  27181  noextendseq  27647  bdayfo  27657  cutsf  27800  addsproplem2  27978  mpteleeOLD  28980  nbuhgr2vtx1edgblem  29436  numclwwlk1lem2foa  30441  shsleji  31457  spansnss  31658  spansncvi  31739  f1o3d  32715  sigaclcu2  34297  measdivcstALTV  34402  dfon2lem6  35999  altxpsspw  36190  hfun  36391  ontgval  36644  ordtoplem  36648  ordcmp  36660  findreccl  36666  bj-xpnzex  37204  bj-snsetex  37208  bj-ismooredr2  37360  bj-ideqg1  37416  topdifinfindis  37598  finxpreclem1  37641  ovoliunnfl  37910  volsupnfl  37913  heibor1lem  38057  heibor1  38058  lshpkrlem1  39483  lfl1dim  39494  leat3  39668  meetat2  39670  glbconxN  39751  pointpsubN  40124  pmapglbx  40142  linepsubclN  40324  dia2dimlem7  41443  dib1dim2  41541  diclspsn  41567  dih1dimatlem  41702  dihatexv2  41712  djhlsmcl  41787  fsuppssind  42948  fltne  42999  3cubes  43044  hbtlem2  43478  hbtlem5  43482  rp-isfinite6  43871  snssiALTVD  45179  snssiALT  45180  elex2VD  45190  elex22VD  45191  fveqvfvv  47397  afv0fv0  47506  lswn0  47801  1neven  48595  cznrng  48618