Theorem wl-sb8mot

Description: Substitution of variable in universal quantifier. Closed form of sb8mo .

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, unfortunately only if x and y are known to be distinct. To avoid any hassle with distinctors, we prefer to derive this theorem independently, ignoring the close connection between both theorems. 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, 11-Aug-2019)

	Ref	Expression
Assertion	wl-sb8mot	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		wl-sb8et	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
2		wl-sb8eut	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	imbi12d	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) )
4		moeu	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
5		moeu	⊢ ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
6	3 4 5	3bitr4g	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )