Description: A weaker form of ax-12 and ax12v , namely the generalization over x of the latter. In this statement, all occurrences of x are bound. (Contributed by BJ, 26-Dec-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ax12v | |- A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax12v | |- ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) |
|
| 2 | 1 | ax-gen | |- A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) |