Theorem brcnvepres

Description: Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018)

	Ref	Expression
Assertion	brcnvepres	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ( ◡ E ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brres	⊢ ( 𝐶 ∈ 𝑊 → ( 𝐵 ( ◡ E ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ◡ E 𝐶 ) ) )
2		brcnvep	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ◡ E 𝐶 ↔ 𝐶 ∈ 𝐵 ) )
3	2	anbi2d	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ◡ E 𝐶 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) )
4	1 3	sylan9bbr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ( ◡ E ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) )