![]() |
Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-sb8motv | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
wl-sb8motv | ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-sb8eft 37531 | . . 3 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)) | |
2 | wl-sb8eutv 37559 | . . 3 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | imbi12d 344 | . 2 ⊢ (∀𝑥Ⅎ𝑦𝜑 → ((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑))) |
4 | moeu 2580 | . 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | |
5 | moeu 2580 | . 2 ⊢ (∃*𝑦[𝑦 / 𝑥]𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑)) | |
6 | 3, 4, 5 | 3bitr4g 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 |