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 37561
Description: Substitution of variable in universal quantifier. Closed form of sb8mo 2598 without ax-13 2374, but requiring 𝑥 and 𝑦 being disjoint.

This theorem relates to wl-mo3t 37556, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2267 and sbco 2509. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 37556 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 37556 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 37531 . . 3 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
2 wl-sb8eutv 37559 . . 3 (∀𝑥𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
31, 2imbi12d 344 . 2 (∀𝑥𝑦𝜑 → ((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑)))
4 moeu 2580 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
5 moeu 2580 . 2 (∃*𝑦[𝑦 / 𝑥]𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑))
63, 4, 53bitr4g 314 1 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1534  wex 1775  wnf 1779  [wsb 2061  ∃*wmo 2535  ∃!weu 2565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-10 2138  ax-11 2154  ax-12 2174
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator