Metamath Proof Explorer

Theorem brressn

Description: Binary relation on a restriction to a singleton. (Contributed by Peter Mazsa, 11-Jun-2024)

Ref Expression
Assertion brressn ⊢ B ∈ V ∧ C ∈ W → B R ↾ A C ↔ B = A ∧ B R C

Proof

Step Hyp Ref Expression
1 brres ⊢ C ∈ W → B R ↾ A C ↔ B ∈ A ∧ B R C
2 1 adantl ⊢ B ∈ V ∧ C ∈ W → B R ↾ A C ↔ B ∈ A ∧ B R C
3 elsng ⊢ B ∈ V → B ∈ A ↔ B = A
4 3 adantr ⊢ B ∈ V ∧ C ∈ W → B ∈ A ↔ B = A
5 4 anbi1d ⊢ B ∈ V ∧ C ∈ W → B ∈ A ∧ B R C ↔ B = A ∧ B R C
6 2 5 bitrd ⊢ B ∈ V ∧ C ∈ W → B R ↾ A C ↔ B = A ∧ B R C