Theorem opthne

Description: Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018)

	Ref	Expression
Hypotheses	opthne.1	|- A e. _V
	opthne.2	|- B e. _V
Assertion	opthne	|- ( <. A , B >. =/= <. C , D >. <-> ( A =/= C \/ B =/= D ) )

Proof

Step	Hyp	Ref	Expression
1		opthne.1	|- A e. _V
2		opthne.2	|- B e. _V
3		opthneg	|- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. =/= <. C , D >. <-> ( A =/= C \/ B =/= D ) ) )
4	1 2 3	mp2an	|- ( <. A , B >. =/= <. C , D >. <-> ( A =/= C \/ B =/= D ) )