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 | |- U. (/) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ss | |- (/) C_ { (/) } |
|
| 2 | uni0b | |- ( U. (/) = (/) <-> (/) C_ { (/) } ) |
|
| 3 | 1 2 | mpbir | |- U. (/) = (/) |