Description: Equality of the coset of B and the coset of C implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm ). (Contributed by Peter Mazsa, 9-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dmecd.1 | |- ( ph -> dom R = A ) |
|
| dmecd.2 | |- ( ph -> [ B ] R = [ C ] R ) |
||
| Assertion | dmecd | |- ( ph -> ( B e. A <-> C e. A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmecd.1 | |- ( ph -> dom R = A ) |
|
| 2 | dmecd.2 | |- ( ph -> [ B ] R = [ C ] R ) |
|
| 3 | 2 | neeq1d | |- ( ph -> ( [ B ] R =/= (/) <-> [ C ] R =/= (/) ) ) |
| 4 | ecdmn0 | |- ( B e. dom R <-> [ B ] R =/= (/) ) |
|
| 5 | ecdmn0 | |- ( C e. dom R <-> [ C ] R =/= (/) ) |
|
| 6 | 3 4 5 | 3bitr4g | |- ( ph -> ( B e. dom R <-> C e. dom R ) ) |
| 7 | 1 | eleq2d | |- ( ph -> ( B e. dom R <-> B e. A ) ) |
| 8 | 1 | eleq2d | |- ( ph -> ( C e. dom R <-> C e. A ) ) |
| 9 | 6 7 8 | 3bitr3d | |- ( ph -> ( B e. A <-> C e. A ) ) |