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 ¬ A / R A dom R

Proof

Step Hyp Ref Expression
1 ecdmn0 x dom R x R
2 1 ralbii x A x dom R x A x R
3 dfss3 A dom R x A x dom R
4 nne ¬ x R x R =
5 4 rexbii x A ¬ x R x A x R =
6 5 notbii ¬ x A ¬ x R ¬ x A x R =
7 dfral2 x A x R ¬ x A ¬ x R
8 0ex V
9 8 elqs A / R x A = x R
10 eqcom = x R x R =
11 10 rexbii x A = x R x A x R =
12 9 11 bitri A / R x A x R =
13 12 notbii ¬ A / R ¬ x A x R =
14 6 7 13 3bitr4ri ¬ A / R x A x R
15 2 3 14 3bitr4ri ¬ A / R A dom R