Theorem 0nelopab

Description: The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017)

	Ref	Expression
Assertion	0nelopab	|- -. (/) e. { <. x , y >. | ph }

Proof

Step	Hyp	Ref	Expression
1		elopab	|- ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
2		nfopab1	|- F/_ x { <. x , y >. | ph }
3	2	nfel2	|- F/ x (/) e. { <. x , y >. | ph }
4	3	nfn	|- F/ x -. (/) e. { <. x , y >. | ph }
5		nfopab2	|- F/_ y { <. x , y >. | ph }
6	5	nfel2	|- F/ y (/) e. { <. x , y >. | ph }
7	6	nfn	|- F/ y -. (/) e. { <. x , y >. | ph }
8		vex	|- x e. _V
9		vex	|- y e. _V
10	8 9	opnzi	|- <. x , y >. =/= (/)
11		nesym	|- ( <. x , y >. =/= (/) <-> -. (/) = <. x , y >. )
12		pm2.21	|- ( -. (/) = <. x , y >. -> ( (/) = <. x , y >. -> -. (/) e. { <. x , y >. | ph } ) )
13	11 12	sylbi	|- ( <. x , y >. =/= (/) -> ( (/) = <. x , y >. -> -. (/) e. { <. x , y >. | ph } ) )
14	10 13	ax-mp	|- ( (/) = <. x , y >. -> -. (/) e. { <. x , y >. | ph } )
15	14	adantr	|- ( ( (/) = <. x , y >. /\ ph ) -> -. (/) e. { <. x , y >. | ph } )
16	7 15	exlimi	|- ( E. y ( (/) = <. x , y >. /\ ph ) -> -. (/) e. { <. x , y >. | ph } )
17	4 16	exlimi	|- ( E. x E. y ( (/) = <. x , y >. /\ ph ) -> -. (/) e. { <. x , y >. | ph } )
18	1 17	sylbi	|- ( (/) e. { <. x , y >. | ph } -> -. (/) e. { <. x , y >. | ph } )
19		id	|- ( -. (/) e. { <. x , y >. | ph } -> -. (/) e. { <. x , y >. | ph } )
20	18 19	pm2.61i	|- -. (/) e. { <. x , y >. | ph }