Metamath Proof Explorer

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