Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Quantifier-free definitions
txprel
Next ⟩
brtxp
Metamath Proof Explorer
Ascii
Unicode
Theorem
txprel
Description:
A tail Cartesian product is a relationship.
(Contributed by
Scott Fenton
, 31-Mar-2012)
Ref
Expression
Assertion
txprel
⊢
Rel
⁡
A
⊗
B
Proof
Step
Hyp
Ref
Expression
1
txpss3v
⊢
A
⊗
B
⊆
V
×
V
×
V
2
xpss
⊢
V
×
V
×
V
⊆
V
×
V
3
1
2
sstri
⊢
A
⊗
B
⊆
V
×
V
4
df-rel
⊢
Rel
⁡
A
⊗
B
↔
A
⊗
B
⊆
V
×
V
5
3
4
mpbir
⊢
Rel
⁡
A
⊗
B