Theorem 2ndnpr

Description: Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017)

	Ref	Expression
Assertion	2ndnpr	|- ( -. A e. ( _V X. _V ) -> ( 2nd ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		2ndval	|- ( 2nd ` A ) = U. ran { A }
2		rnsnn0	|- ( A e. ( _V X. _V ) <-> ran { A } =/= (/) )
3	2	biimpri	|- ( ran { A } =/= (/) -> A e. ( _V X. _V ) )
4	3	necon1bi	|- ( -. A e. ( _V X. _V ) -> ran { A } = (/) )
5	4	unieqd	|- ( -. A e. ( _V X. _V ) -> U. ran { A } = U. (/) )
6		uni0	|- U. (/) = (/)
7	5 6	eqtrdi	|- ( -. A e. ( _V X. _V ) -> U. ran { A } = (/) )
8	1 7	syl5eq	|- ( -. A e. ( _V X. _V ) -> ( 2nd ` A ) = (/) )