Theorem aovov0bi

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

	Ref	Expression
Assertion	aovov0bi	⊢ ( ( 𝐴 𝐹 𝐵 ) = ∅ ↔ ( (( 𝐴 𝐹 𝐵 )) = ∅ ∨ (( 𝐴 𝐹 𝐵 )) = V ) )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2	1	eqeq1i	⊢ ( ( 𝐴 𝐹 𝐵 ) = ∅ ↔ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
3		afvfv0bi	⊢ ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ↔ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ∨ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V ) )
4		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
5	4	eqeq1i	⊢ ( (( 𝐴 𝐹 𝐵 )) = ∅ ↔ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
6	5	bicomi	⊢ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ↔ (( 𝐴 𝐹 𝐵 )) = ∅ )
7	4	eqeq1i	⊢ ( (( 𝐴 𝐹 𝐵 )) = V ↔ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V )
8	7	bicomi	⊢ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V ↔ (( 𝐴 𝐹 𝐵 )) = V )
9	6 8	orbi12i	⊢ ( ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ ∨ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V ) ↔ ( (( 𝐴 𝐹 𝐵 )) = ∅ ∨ (( 𝐴 𝐹 𝐵 )) = V ) )
10	2 3 9	3bitri	⊢ ( ( 𝐴 𝐹 𝐵 ) = ∅ ↔ ( (( 𝐴 𝐹 𝐵 )) = ∅ ∨ (( 𝐴 𝐹 𝐵 )) = V ) )