Theorem n0elqs

Description: Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019)

	Ref	Expression
Assertion	n0elqs	|- ( -. (/) e. ( A /. R ) <-> A C_ dom R )

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	|- ( x e. dom R <-> [ x ] R =/= (/) )
2	1	ralbii	|- ( A. x e. A x e. dom R <-> A. x e. A [ x ] R =/= (/) )
3		dfss3	|- ( A C_ dom R <-> A. x e. A x e. dom R )
4		nne	|- ( -. [ x ] R =/= (/) <-> [ x ] R = (/) )
5	4	rexbii	|- ( E. x e. A -. [ x ] R =/= (/) <-> E. x e. A [ x ] R = (/) )
6	5	notbii	|- ( -. E. x e. A -. [ x ] R =/= (/) <-> -. E. x e. A [ x ] R = (/) )
7		dfral2	|- ( A. x e. A [ x ] R =/= (/) <-> -. E. x e. A -. [ x ] R =/= (/) )
8		0ex	|- (/) e. _V
9	8	elqs	|- ( (/) e. ( A /. R ) <-> E. x e. A (/) = [ x ] R )
10		eqcom	|- ( (/) = [ x ] R <-> [ x ] R = (/) )
11	10	rexbii	|- ( E. x e. A (/) = [ x ] R <-> E. x e. A [ x ] R = (/) )
12	9 11	bitri	|- ( (/) e. ( A /. R ) <-> E. x e. A [ x ] R = (/) )
13	12	notbii	|- ( -. (/) e. ( A /. R ) <-> -. E. x e. A [ x ] R = (/) )
14	6 7 13	3bitr4ri	|- ( -. (/) e. ( A /. R ) <-> A. x e. A [ x ] R =/= (/) )
15	2 3 14	3bitr4ri	|- ( -. (/) e. ( A /. R ) <-> A C_ dom R )