Theorem brovpreldm

Description: If a binary relation holds for the result of an operation, the operands are in the domain of the operation. (Contributed by AV, 31-Dec-2020)

	Ref	Expression
Assertion	brovpreldm	⊢ ( 𝐷 ( 𝐵 𝐴 𝐶 ) 𝐸 → ⟨ 𝐵 , 𝐶 ⟩ ∈ dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐷 ( 𝐵 𝐴 𝐶 ) 𝐸 ↔ ⟨ 𝐷 , 𝐸 ⟩ ∈ ( 𝐵 𝐴 𝐶 ) )
2		ne0i	⊢ ( ⟨ 𝐷 , 𝐸 ⟩ ∈ ( 𝐵 𝐴 𝐶 ) → ( 𝐵 𝐴 𝐶 ) ≠ ∅ )
3		df-ov	⊢ ( 𝐵 𝐴 𝐶 ) = ( 𝐴 ‘ ⟨ 𝐵 , 𝐶 ⟩ )
4		ndmfv	⊢ ( ¬ ⟨ 𝐵 , 𝐶 ⟩ ∈ dom 𝐴 → ( 𝐴 ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = ∅ )
5	3 4	syl5eq	⊢ ( ¬ ⟨ 𝐵 , 𝐶 ⟩ ∈ dom 𝐴 → ( 𝐵 𝐴 𝐶 ) = ∅ )
6	5	necon1ai	⊢ ( ( 𝐵 𝐴 𝐶 ) ≠ ∅ → ⟨ 𝐵 , 𝐶 ⟩ ∈ dom 𝐴 )
7	2 6	syl	⊢ ( ⟨ 𝐷 , 𝐸 ⟩ ∈ ( 𝐵 𝐴 𝐶 ) → ⟨ 𝐵 , 𝐶 ⟩ ∈ dom 𝐴 )
8	1 7	sylbi	⊢ ( 𝐷 ( 𝐵 𝐴 𝐶 ) 𝐸 → ⟨ 𝐵 , 𝐶 ⟩ ∈ dom 𝐴 )