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  4457  reusv3  4507  fvmptt  5671  releldm2  6271  qsid  6687  rerecclap  8803  nndiv  9077  zq  9747  4fvwrd4  10262  conjnmzb  13616  bj-bdcel  15773