Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
relin1
Next ⟩
relin2
Metamath Proof Explorer
Ascii
Unicode
Theorem
relin1
Description:
The intersection with a relation is a relation.
(Contributed by
NM
, 16-Aug-1994)
Ref
Expression
Assertion
relin1
⊢
Rel
⁡
A
→
Rel
⁡
A
∩
B
Proof
Step
Hyp
Ref
Expression
1
inss1
⊢
A
∩
B
⊆
A
2
relss
⊢
A
∩
B
⊆
A
→
Rel
⁡
A
→
Rel
⁡
A
∩
B
3
1
2
ax-mp
⊢
Rel
⁡
A
→
Rel
⁡
A
∩
B