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 253	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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

This theorem is used by:  elex22  3475  disjne  4408  rabsneq  4603  elpr2g  4610  eqoreldif  4646  ordelinel  6465  onun2  6472  ssimaex  6968  fnex  7221  f1ocnv2d  7672  omun  7897  peano5  7903  mpoexw  8089  tfrlem8  8385  tz7.48-2  8445  tz7.49  8448  eroprf  8829  pssnn  9177  onfin  9223  ac6sfi  9268  elfiun  9415  brwdom  9554  hfunOLD  9912  ficardom  10035  ficard  10642  tskxpss  10850  inar1  10853  rankcf  10855  tskuni  10861  gruun  10884  nsmallnq  11055  prnmadd  11075  genpss  11082  mpoaddf  11287  mpomulf  11288  eqlei  11413  eqlei2  11414  renegcli  11612  supaddc  12277  supadd  12278  supmul1  12279  supmullem2  12281  supmul  12282  nn0ind-raph  12792  uzwo  13031  iccid  13514  hashvnfin  14497  hashdifsnp1  14644  mertenslem2  16047  4sqlem1  17119  4sqlem4  17123  4sqlem11  17126  symggen  19677  psgnran  19722  odlem1  19742  gexlem1  19786  gsumpr  20162  lssvneln0  21220  lss1d  21231  lspsn  21270  lsmelval2  21353  rnglidlmmgm  21526  psgnghm  21879  opnneiid  23437  cmpsublem  23710  metrest  24836  metustel  24862  dscopn  24885  ovolshftlem2  25824  subopnmbl  25918  deg1ldgn  26404  plyremlem  26618  coseq0negpitopi  26825  ppiublem1  27522  fltne  27968  noextendseq  28017  bdayfo  28027  cutsf  28171  addsproplem2  28349  mpteleeOLD  29466  nbuhgr2vtx1edgblem  29925  numclwwlk1lem2foa  30948  shsleji  31965  spansnss  32166  spansncvi  32247  f1o3d  33213  sigaclcu2  34745  measdivcstALTV  34851  kardfi  35821  dfon2lem6  36530  altxpsspw  36722  ontgval  37199  ordtoplem  37203  ordcmp  37215  findreccl  37221  bj-xpnzex  37852  bj-snsetex  37856  bj-ismooredr2  38011  bj-ideqg1  38065  topdifinfindis  38249  finxpreclem1  38292  ovoliunnfl  38560  volsupnfl  38563  heibor1lem  38723  heibor1  38724  lshpkrlem1  40147  lfl1dim  40158  leat3  40332  meetat2  40334  glbconxN  40415  pointpsubN  40788  pmapglbx  40806  linepsubclN  40988  dia2dimlem7  42107  dib1dim2  42205  diclspsn  42231  dih1dimatlem  42366  dihatexv2  42376  djhlsmcl  42451  fsuppssind  43601  3cubes  43680  hbtlem2  44110  hbtlem5  44114  rp-isfinite6  44503  snssiALTVD  45794  snssiALT  45795  elex2VD  45805  elex22VD  45806  fveqvfvv  48079  afv0fv0  48188  lswn0  48495  1neven  49304  cznrng  49327