Theorem fvnonrel

Description: The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020)

	Ref	Expression
Assertion	fvnonrel	|- ( ( A \ `' `' A ) ` X ) = (/)

Proof

Step	Hyp	Ref	Expression
1		fvrn0	|- ( ( A \ `' `' A ) ` X ) e. ( ran ( A \ `' `' A ) u. { (/) } )
2		rnnonrel	|- ran ( A \ `' `' A ) = (/)
3		0ss	|- (/) C_ { (/) }
4	2 3	eqsstri	|- ran ( A \ `' `' A ) C_ { (/) }
5		ssequn1	|- ( ran ( A \ `' `' A ) C_ { (/) } <-> ( ran ( A \ `' `' A ) u. { (/) } ) = { (/) } )
6	4 5	mpbi	|- ( ran ( A \ `' `' A ) u. { (/) } ) = { (/) }
7	1 6	eleqtri	|- ( ( A \ `' `' A ) ` X ) e. { (/) }
8		fvex	|- ( ( A \ `' `' A ) ` X ) e. _V
9	8	elsn	|- ( ( ( A \ `' `' A ) ` X ) e. { (/) } <-> ( ( A \ `' `' A ) ` X ) = (/) )
10	7 9	mpbi	|- ( ( A \ `' `' A ) ` X ) = (/)