Theorem aovpcov0

Description: If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	aovpcov0	⊢ ( (( 𝐴 𝐹 𝐵 )) = V → ( 𝐴 𝐹 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		afvpcfv0	⊢ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
2		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
3	2	eqeq1i	⊢ ( (( 𝐴 𝐹 𝐵 )) = V ↔ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V )
4		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
5	4	eqeq1i	⊢ ( ( 𝐴 𝐹 𝐵 ) = ∅ ↔ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
6	1 3 5	3imtr4i	⊢ ( (( 𝐴 𝐹 𝐵 )) = V → ( 𝐴 𝐹 𝐵 ) = ∅ )