Description: A condition where the converse of xpex holds as well. Corollary 6.9(2) in TakeutiZaring p. 26. (Contributed by Andrew Salmon, 13-Nov-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xpexcnv | |- ( ( B =/= (/) /\ ( A X. B ) e. _V ) -> A e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmexg | |- ( ( A X. B ) e. _V -> dom ( A X. B ) e. _V ) |
|
| 2 | dmxp | |- ( B =/= (/) -> dom ( A X. B ) = A ) |
|
| 3 | 2 | eleq1d | |- ( B =/= (/) -> ( dom ( A X. B ) e. _V <-> A e. _V ) ) |
| 4 | 1 3 | syl5ib | |- ( B =/= (/) -> ( ( A X. B ) e. _V -> A e. _V ) ) |
| 5 | 4 | imp | |- ( ( B =/= (/) /\ ( A X. B ) e. _V ) -> A e. _V ) |