Description: In the case of sbt , the hypothesis in df-sb is derivable from propositional axioms and ax-gen alone. The essential proof step is presented in this lemma. (Contributed by Wolf Lammen, 4-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbtlem.1 | |- ph |
|
| Assertion | sbtlem | |- A. y ( y = t -> A. x ( x = y -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbtlem.1 | |- ph |
|
| 2 | 1 | a1i | |- ( x = y -> ph ) |
| 3 | 2 | ax-gen | |- A. x ( x = y -> ph ) |
| 4 | 3 | a1i | |- ( y = t -> A. x ( x = y -> ph ) ) |
| 5 | 4 | ax-gen | |- A. y ( y = t -> A. x ( x = y -> ph ) ) |