Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
brinxprnres
Next ⟩
inxprnres
Metamath Proof Explorer
Ascii
Unicode
Theorem
brinxprnres
Description:
Binary relation on a restriction.
(Contributed by
Peter Mazsa
, 2-Jan-2019)
Ref
Expression
Assertion
brinxprnres
⊢
C
∈
V
→
B
R
∩
A
×
ran
⁡
R
↾
A
C
↔
B
∈
A
∧
B
R
C
Proof
Step
Hyp
Ref
Expression
1
brres2
⊢
B
R
↾
A
C
↔
B
R
∩
A
×
ran
⁡
R
↾
A
C
2
brres
⊢
C
∈
V
→
B
R
↾
A
C
↔
B
∈
A
∧
B
R
C
3
1
2
bitr3id
⊢
C
∈
V
→
B
R
∩
A
×
ran
⁡
R
↾
A
C
↔
B
∈
A
∧
B
R
C