Description: A range Cartesian product is a relation. This is Scott Fenton's txprel with a different symbol, see https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xrnrel | |- Rel ( A |X. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xrnss3v | |- ( A |X. B ) C_ ( _V X. ( _V X. _V ) ) |
|
| 2 | xpss | |- ( _V X. ( _V X. _V ) ) C_ ( _V X. _V ) |
|
| 3 | 1 2 | sstri | |- ( A |X. B ) C_ ( _V X. _V ) |
| 4 | df-rel | |- ( Rel ( A |X. B ) <-> ( A |X. B ) C_ ( _V X. _V ) ) |
|
| 5 | 3 4 | mpbir | |- Rel ( A |X. B ) |