Theorem aov0nbovbi

Description: The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	aov0nbovbi	|- ( (/) e/ C -> ( (( A F B )) e. C <-> ( A F B ) e. C ) )

Proof

Step	Hyp	Ref	Expression
1		afv0nbfvbi	|- ( (/) e/ C -> ( ( F ''' <. A , B >. ) e. C <-> ( F ` <. A , B >. ) e. C ) )
2		df-aov	|- (( A F B )) = ( F ''' <. A , B >. )
3	2	eleq1i	|- ( (( A F B )) e. C <-> ( F ''' <. A , B >. ) e. C )
4		df-ov	|- ( A F B ) = ( F ` <. A , B >. )
5	4	eleq1i	|- ( ( A F B ) e. C <-> ( F ` <. A , B >. ) e. C )
6	1 3 5	3bitr4g	|- ( (/) e/ C -> ( (( A F B )) e. C <-> ( A F B ) e. C ) )