Metamath Proof Explorer

Theorem risset

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

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

Proof

Step Hyp Ref Expression
1 exancom 
 |-  ( E. x ( x e. B /\ x = A ) <-> E. x ( x = A /\ x e. B ) )
2 df-rex 
 |-  ( E. x e. B x = A <-> E. x ( x e. B /\ x = A ) )
3 dfclel 
 |-  ( A e. B <-> E. x ( x = A /\ x e. B ) )
4 1 2 3 3bitr4ri 
 |-  ( A e. B <-> E. x e. B x = A )