Description: Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | issetid | |- ( A e. _V <-> A _I A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ididg | |- ( A e. _V -> A _I A ) |
|
| 2 | reli | |- Rel _I |
|
| 3 | 2 | brrelex1i | |- ( A _I A -> A e. _V ) |
| 4 | 1 3 | impbii | |- ( A e. _V <-> A _I A ) |