Theorem risset 2534

Description: Two ways to say " A belongs to B". (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
risset	|- ( A e. B <-> E. x e. B x = A )

Distinct variable groups:   x, A   x, B

Proof of Theorem risset

Step	Hyp	Ref	Expression
1		exancom 1631	. 2 |- ( E. x ( x e. B /\ x = A ) <-> E. x ( x = A /\ x e. B ) )
2		df-rex 2490	. 2 |- ( E. x e. B x = A <-> E. x ( x e. B /\ x = A ) )
3		df-clel 2201	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
4	1, 2, 3	3bitr4ri 213	1 |- ( A e. B <-> E. x e. B x = A )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   E.wex 1515   e. wcel 2176   E.wrex 2485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-clel 2201  df-rex 2490

This theorem is referenced by:  clel5  2910  reueq  2972  reuind  2978  0el  3483  iunid  3983  sucel  4458  reusv3  4508  fvmptt  5673  releldm2  6273  qsid  6689  rerecclap  8805  nndiv  9079  zq  9749  4fvwrd4  10264  conjnmzb  13649  bj-bdcel  15810