Theorem eleq1a 2540

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 2529	. 2
2	1	biimprcd 225	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818

This theorem is referenced by:  elex2  3121  elex22  3122  reu6  3288  disjne  3872  ssimaex  5938  fnex  6139  f1ocnv2d  6526  peano5  6723  tfrlem8  7072  tz7.48-2  7126  tz7.49  7129  eroprf  7428  onfin  7728  pssnn  7758  ac6sfi  7784  elfiun  7910  brwdom  8014  ficardom  8363  ficard  8961  tskxpss  9171  inar1  9174  rankcf  9176  tskuni  9182  gruun  9205  nsmallnq  9376  prnmadd  9396  genpss  9403  eqlei  9715  eqlei2  9716  renegcli  9903  supmul1  10533  supmullem2  10535  supmul  10536  nn0ind-raph  10989  uzwo  11173  uzwoOLD  11174  iccid  11603  hashvnfin  12431  brfi1indlem  12531  mertenslem2  13694  4sqlem1  14466  4sqlem4  14470  4sqlem11  14473  symggen  16495  psgnran  16540  odlem1  16559  gexlem1  16599  lssneln0  17598  lss1d  17609  lspsn  17648  lsmelval2  17731  psgnghm  18616  opnneiid  19627  cmpsublem  19899  metrest  21027  metustelOLD  21054  metustel  21055  dscopn  21094  ovolshftlem2  21921  subopnmbl  22013  deg1ldgn  22493  plyremlem  22700  coseq0negpitopi  22896  ppiublem1  23477  mptelee  24198  frgrancvvdeqlem1  25030  frgrawopreglem4  25047  shsleji  26288  spansnss  26489  spansncvi  26570  f1o3d  27471  sigaclcu2  28120  measdivcstOLD  28195  dfon2lem6  29220  bdayfo  29435  altxpsspw  29627  hfun  29835  ontgval  29896  ordtoplem  29900  ordcmp  29912  findreccl  29918  supaddc  30041  supadd  30042  ovoliunnfl  30056  volsupnfl  30059  heibor1lem  30305  heibor1  30306  hbtlem2  31073  hbtlem5  31077  fveqvfvv  32209  afv0fv0  32234  lswn0  32343  lidlmmgm  32731  1neven  32738  cznrng  32763  gsumpr  32950  snssiALTVD  33627  snssiALT  33628  elex2VD  33638  elex22VD  33639  bj-xpnzex  34516  bj-snsetex  34521  lshpkrlem1  34835  lfl1dim  34846  leat3  35020  meetat2  35022  glbconxN  35102  pointpsubN  35475  pmapglbx  35493  linepsubclN  35675  dia2dimlem7  36797  dib1dim2  36895  diclspsn  36921  dih1dimatlem  37056  dihatexv2  37066  djhlsmcl  37141  rp-isfinite6  37744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452