Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elimasn.1 | |- B e. _V |
|
elimasn.2 | |- C e. _V |
||
Assertion | elimasn | |- ( C e. ( A " { B } ) <-> <. B , C >. e. A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elimasn.1 | |- B e. _V |
|
2 | elimasn.2 | |- C e. _V |
|
3 | breq2 | |- ( x = C -> ( B A x <-> B A C ) ) |
|
4 | imasng | |- ( B e. _V -> ( A " { B } ) = { x | B A x } ) |
|
5 | 1 4 | ax-mp | |- ( A " { B } ) = { x | B A x } |
6 | 2 3 5 | elab2 | |- ( C e. ( A " { B } ) <-> B A C ) |
7 | df-br | |- ( B A C <-> <. B , C >. e. A ) |
|
8 | 6 7 | bitri | |- ( C e. ( A " { B } ) <-> <. B , C >. e. A ) |