NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-9o Unicode version

Axiom ax-9o 2138
Description: A variant of ax9 1949. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint).

This axiom is obsolete and should no longer be used. It is proved above as theorem ax9o 1950. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

Assertion
Ref Expression
ax-9o

Detailed syntax breakdown of Axiom ax-9o
StepHypRef Expression
1 vx . . . . 5
2 vy . . . . 5
31, 2weq 1643 . . . 4
4 wph . . . . 5
54, 1wal 1540 . . . 4
63, 5wi 4 . . 3
76, 1wal 1540 . 2
87, 4wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  ax9from9o  2148  equid1  2158  equid1ALT  2176
  Copyright terms: Public domain W3C validator