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	⊢ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		fvrn0	⊢ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) ∈ ( ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) ∪ { ∅ } )
2		rnnonrel	⊢ ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅
3		0ss	⊢ ∅ ⊆ { ∅ }
4	2 3	eqsstri	⊢ ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) ⊆ { ∅ }
5		ssequn1	⊢ ( ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) ⊆ { ∅ } ↔ ( ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) ∪ { ∅ } ) = { ∅ } )
6	4 5	mpbi	⊢ ( ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) ∪ { ∅ } ) = { ∅ }
7	1 6	eleqtri	⊢ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) ∈ { ∅ }
8		fvex	⊢ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) ∈ V
9	8	elsn	⊢ ( ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) ∈ { ∅ } ↔ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) = ∅ )
10	7 9	mpbi	⊢ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ‘ 𝑋 ) = ∅