Metamath Proof Explorer


Theorem uni0OLD

Description: Obsolete version of uni0 as of 1-Feb-2026. (Contributed by NM, 16-Sep-1993) Remove use of ax-nul . (Revised by Eric Schmidt, 4-Apr-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion uni0OLD =

Proof

Step Hyp Ref Expression
1 0ss
2 uni0b =
3 1 2 mpbir =