Metamath Proof Explorer


Theorem chocnul

Description: Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000) (New usage is discouraged.)

Ref Expression
Assertion chocnul =

Proof

Step Hyp Ref Expression
1 ral0 y x ih y = 0
2 0ss
3 ocel x x y x ih y = 0
4 2 3 ax-mp x x y x ih y = 0
5 1 4 mpbiran2 x x
6 5 eqriv =