Theorem elnonrel

Description: Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020)

	Ref	Expression
Assertion	elnonrel	|- ( <. X , Y >. e. ( A \ `' `' A ) <-> ( (/) e. A /\ -. ( X e. _V /\ Y e. _V ) ) )

Proof

Step	Hyp	Ref	Expression
1		nonrel	|- ( A \ `' `' A ) = ( A \ ( _V X. _V ) )
2	1	eleq2i	|- ( <. X , Y >. e. ( A \ `' `' A ) <-> <. X , Y >. e. ( A \ ( _V X. _V ) ) )
3		eldif	|- ( <. X , Y >. e. ( A \ ( _V X. _V ) ) <-> ( <. X , Y >. e. A /\ -. <. X , Y >. e. ( _V X. _V ) ) )
4		opelxp	|- ( <. X , Y >. e. ( _V X. _V ) <-> ( X e. _V /\ Y e. _V ) )
5	4	notbii	|- ( -. <. X , Y >. e. ( _V X. _V ) <-> -. ( X e. _V /\ Y e. _V ) )
6	5	anbi2i	|- ( ( <. X , Y >. e. A /\ -. <. X , Y >. e. ( _V X. _V ) ) <-> ( <. X , Y >. e. A /\ -. ( X e. _V /\ Y e. _V ) ) )
7		opprc	|- ( -. ( X e. _V /\ Y e. _V ) -> <. X , Y >. = (/) )
8	7	eleq1d	|- ( -. ( X e. _V /\ Y e. _V ) -> ( <. X , Y >. e. A <-> (/) e. A ) )
9	8	pm5.32ri	|- ( ( <. X , Y >. e. A /\ -. ( X e. _V /\ Y e. _V ) ) <-> ( (/) e. A /\ -. ( X e. _V /\ Y e. _V ) ) )
10	6 9	bitri	|- ( ( <. X , Y >. e. A /\ -. <. X , Y >. e. ( _V X. _V ) ) <-> ( (/) e. A /\ -. ( X e. _V /\ Y e. _V ) ) )
11	3 10	bitri	|- ( <. X , Y >. e. ( A \ ( _V X. _V ) ) <-> ( (/) e. A /\ -. ( X e. _V /\ Y e. _V ) ) )
12	2 11	bitri	|- ( <. X , Y >. e. ( A \ `' `' A ) <-> ( (/) e. A /\ -. ( X e. _V /\ Y e. _V ) ) )