Theorem opelvvdif

Description: Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019)

	Ref	Expression
Assertion	opelvvdif	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( ( _V X. _V ) \ R ) <-> -. <. A , B >. e. R ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( <. A , B >. e. ( ( _V X. _V ) \ R ) <-> ( <. A , B >. e. ( _V X. _V ) /\ -. <. A , B >. e. R ) )
2		opelvvg	|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )
3	2	biantrurd	|- ( ( A e. V /\ B e. W ) -> ( -. <. A , B >. e. R <-> ( <. A , B >. e. ( _V X. _V ) /\ -. <. A , B >. e. R ) ) )
4	1 3	bitr4id	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. ( ( _V X. _V ) \ R ) <-> -. <. A , B >. e. R ) )