Theorem 1stnpr

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

	Ref	Expression
Assertion	1stnpr	|- ( -. A e. ( _V X. _V ) -> ( 1st ` A ) = (/) )

Proof

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