Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-sb8motv Structured version   Visualization version   GIF version

Theorem wl-sb8motv 37582
Description: Substitution of variable in universal quantifier. Closed form of sb8mo 2601 without ax-13 2377, but requiring 𝑥 and 𝑦 being disjoint.

This theorem relates to wl-mo3t 37577, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2270 and sbco 2512. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 37577 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 37577 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
StepHypRef Expression
1 wl-sb8eft 37552 . . 3 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
2 wl-sb8eutv 37580 . . 3 (∀𝑥𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
31, 2imbi12d 344 . 2 (∀𝑥𝑦𝜑 → ((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑)))
4 moeu 2583 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5 moeu 2583 . 2 (∃*𝑦[𝑦 / 𝑥]𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑))
63, 4, 53bitr4g 314 1 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wex 1779  wnf 1783  [wsb 2064  ∃*wmo 2538  ∃!weu 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator