Theorem spr0el

Description: The empty set is not an unordered pair over any set V . (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	spr0el	|- (/) e/ ( Pairs ` V )

Proof

Step	Hyp	Ref	Expression
1		spr0nelg	|- (/) e/ { p | E. a E. b p = { a , b } }
2		sprssspr	|- ( Pairs ` V ) C_ { p | E. a E. b p = { a , b } }
3	2	sseli	|- ( (/) e. ( Pairs ` V ) -> (/) e. { p | E. a E. b p = { a , b } } )
4	3	con3i	|- ( -. (/) e. { p | E. a E. b p = { a , b } } -> -. (/) e. ( Pairs ` V ) )
5		df-nel	|- ( (/) e/ { p | E. a E. b p = { a , b } } <-> -. (/) e. { p | E. a E. b p = { a , b } } )
6		df-nel	|- ( (/) e/ ( Pairs ` V ) <-> -. (/) e. ( Pairs ` V ) )
7	4 5 6	3imtr4i	|- ( (/) e/ { p | E. a E. b p = { a , b } } -> (/) e/ ( Pairs ` V ) )
8	1 7	ax-mp	|- (/) e/ ( Pairs ` V )