Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)
Ref | Expression | ||
---|---|---|---|
Hypotheses | inf3lem.1 | |
|
inf3lem.2 | |
||
inf3lem.3 | |
||
inf3lem.4 | |
||
Assertion | inf3lemb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inf3lem.1 | |
|
2 | inf3lem.2 | |
|
3 | inf3lem.3 | |
|
4 | inf3lem.4 | |
|
5 | 2 | fveq1i | |
6 | 0ex | |
|
7 | fr0g | |
|
8 | 6 7 | ax-mp | |
9 | 5 8 | eqtri | |