Theorem brres

Description: Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022)

	Ref	Expression
Assertion	brres	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opelres	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) )
2		df-br	⊢ ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 ↾ 𝐴 ) )
3		df-br	⊢ ( 𝐵 𝑅 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 )
4	3	anbi2i	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) )
5	1 2 4	3bitr4g	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐵 ( 𝑅 ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝐶 ) ) )