Description: A lemma used to prove a weak version of the axiom of substitution ax-12 . (Temporary comment: The general statement that ax12wlem proves.) (Contributed by BJ, 20-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-ax12wlem.1 | |
|
Assertion | bj-ax12wlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-ax12wlem.1 | |
|
2 | ax-5 | |
|
3 | 1 2 | bj-ax12i | |