This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )