Theorem eleq1a 2856

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  elex22  3477  disjne  4406  rabsneq  4598  elpr2g  4605  eqoreldif  4641  ordelinel  6443  onun2  6450  ssimaex  6946  fnex  7195  f1ocnv2d  7643  omun  7862  peano5  7868  mpoexw  8053  tfrlem8  8348  tz7.48-2  8406  tz7.49  8409  eroprf  8790  pssnn  9130  onfin  9176  ac6sfi  9221  elfiun  9369  brwdom  9508  ficardom  9912  ficard  10515  tskxpss  10723  inar1  10726  rankcf  10728  tskuni  10734  gruun  10757  nsmallnq  10928  prnmadd  10948  genpss  10955  mpoaddf  11160  mpomulf  11161  eqlei  11286  eqlei2  11287  renegcli  11485  supaddc  12152  supadd  12153  supmul1  12154  supmullem2  12156  supmul  12157  nn0ind-raph  12666  uzwo  12905  iccid  13387  hashvnfin  14366  hashdifsnp1  14512  mertenslem2  15905  4sqlem1  16974  4sqlem4  16978  4sqlem11  16981  symggen  19500  psgnran  19545  odlem1  19565  gexlem1  19609  gsumpr  19985  lssvneln0  21006  lss1d  21017  lspsn  21056  lsmelval2  21139  rnglidlmmgm  21302  psgnghm  21619  opnneiid  23173  cmpsublem  23446  metrest  24571  metustel  24597  dscopn  24620  ovolshftlem2  25559  subopnmbl  25653  deg1ldgn  26140  plyremlem  26355  coseq0negpitopi  26555  ppiublem1  27253  noextendseq  27718  bdayfo  27728  cutsf  27872  addsproplem2  28050  mpteleeOLD  29052  nbuhgr2vtx1edgblem  29508  numclwwlk1lem2foa  30512  shsleji  31529  spansnss  31730  spansncvi  31811  f1o3d  32788  sigaclcu2  34377  measdivcstALTV  34482  dfon2lem6  36096  altxpsspw  36287  hfun  36488  ontgval  36751  ordtoplem  36755  ordcmp  36767  findreccl  36773  bj-xpnzex  37404  bj-snsetex  37408  bj-ismooredr2  37560  bj-ideqg1  37616  topdifinfindis  37800  finxpreclem1  37843  ovoliunnfl  38121  volsupnfl  38124  heibor1lem  38268  heibor1  38269  lshpkrlem1  39694  lfl1dim  39705  leat3  39879  meetat2  39881  glbconxN  39962  pointpsubN  40335  pmapglbx  40353  linepsubclN  40535  dia2dimlem7  41654  dib1dim2  41752  diclspsn  41778  dih1dimatlem  41913  dihatexv2  41923  djhlsmcl  41998  fsuppssind  43135  fltne  43186  3cubes  43231  hbtlem2  43661  hbtlem5  43665  rp-isfinite6  44054  snssiALTVD  45362  snssiALT  45363  elex2VD  45373  elex22VD  45374  fveqvfvv  47594  afv0fv0  47703  lswn0  48010  1neven  48820  cznrng  48843