Metamath Proof Explorer


Theorem brinxprnres

Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019)

Ref Expression
Assertion brinxprnres ( 𝐶𝑉 → ( 𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) 𝐶 ↔ ( 𝐵𝐴𝐵 𝑅 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 brres2 ( 𝐵 ( 𝑅𝐴 ) 𝐶𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) 𝐶 )
2 brres ( 𝐶𝑉 → ( 𝐵 ( 𝑅𝐴 ) 𝐶 ↔ ( 𝐵𝐴𝐵 𝑅 𝐶 ) ) )
3 1 2 bitr3id ( 𝐶𝑉 → ( 𝐵 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) 𝐶 ↔ ( 𝐵𝐴𝐵 𝑅 𝐶 ) ) )