Description: An equivalence relation is a set if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010) (Proof shortened by Mario Carneiro, 12-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | erex | |- ( R Er A -> ( A e. V -> R e. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | erssxp | |- ( R Er A -> R C_ ( A X. A ) ) |
|
| 2 | sqxpexg | |- ( A e. V -> ( A X. A ) e. _V ) |
|
| 3 | ssexg | |- ( ( R C_ ( A X. A ) /\ ( A X. A ) e. _V ) -> R e. _V ) |
|
| 4 | 1 2 3 | syl2an | |- ( ( R Er A /\ A e. V ) -> R e. _V ) |
| 5 | 4 | ex | |- ( R Er A -> ( A e. V -> R e. _V ) ) |