Description: Substitution of variable in universal quantifier. Closed form of sb8mo without ax-13 , but requiring x and y being disjoint.
This theorem relates to wl-mo3t , since replacing ph with [ y / x ] ph in the latter yields subexpressions like [ x / y ] [ y / x ] ph , which can be reduced to ph via sbft and sbco . So E* x ph <-> E* y [ y / x ] ph is provable from wl-mo3t in a simple fashion. From an educational standpoint, one would assume wl-mo3t to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 3-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-sb8motv | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wl-sb8eft | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
| 2 | wl-sb8eutv | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
| 3 | 1 2 | imbi12d | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) ) |
| 4 | moeu | ⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ) | |
| 5 | moeu | ⊢ ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
| 6 | 3 4 5 | 3bitr4g | ⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) |