Theorem wl-sb8motv 37632

Description: Substitution of variable in universal quantifier. Closed form of sb8mo 2596 without ax-13 2372, but requiring 𝑥 and 𝑦 being disjoint.

This theorem relates to wl-mo3t 37627, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2272 and sbco 2507. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 37627 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 37627 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.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem wl-sb8motv

Step	Hyp	Ref	Expression
1		wl-sb8eft 37602	. . 3 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
2		wl-sb8eutv 37630	. . 3 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
3	1, 2	imbi12d 344	. 2 ⊢ (∀𝑥Ⅎ𝑦𝜑 → ((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑)))
4		moeu 2578	. 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5		moeu 2578	. 2 ⊢ (∃*𝑦[𝑦 / 𝑥]𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑))
6	3, 4, 5	3bitr4g 314	1 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784  [wsb 2067  ∃*wmo 2533  ∃!weu 2563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564

This theorem is referenced by: (None)