| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: A variant of ax-9 1624.
Axiom scheme C10' in [Megill] p. 448 (p. 16 of
the
preprint).
This axiom is redundant, as shown by theorem ax9o 1791. |
| Ref | Expression |
|---|---|
| ax-9o |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx |
. . . . . 6
| |
| 2 | 1 | cv 1614 |
. . . . 5
|
| 3 | vy |
. . . . . 6
| |
| 4 | 3 | cv 1614 |
. . . . 5
|
| 5 | 2, 4 | wceq 1615 |
. . . 4
|
| 6 | wph |
. . . . 5
| |
| 7 | 6, 1 | wal 1613 |
. . . 4
|
| 8 | 5, 7 | wi 3 |
. . 3
|
| 9 | 8, 1 | wal 1613 |
. 2
|
| 10 | 9, 6 | wi 3 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: ax9 1793 equid 1795 equs4 1820 equsal 1821 a4imt 1829 a4im 1830 cbv1 1833 |