Theorem eleq12 2533

Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)

Assertion

Ref	Expression
eleq12

Proof of Theorem eleq12

Step	Hyp	Ref	Expression
1		eleq1 2529	. 2
2		eleq2 2530	. 2
3	1, 2	sylan9bb 699	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818

This theorem is referenced by:  trel  4552  pwnss  4617  epelg  4797  preleq  8055  oemapval  8123  cantnf  8133  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  nnsdomel  8392  cldval  19524  isufil  20404  issiga  28111  wepwsolem  30987  aomclem8  31007

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