![]() |
Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-sb8mot | Structured version Visualization version GIF version |
Description: Substitution of variable
in universal quantifier. Closed form of
sb8mo 2662.
This theorem relates to wl-mo3t 34977, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2267 and sbco 2526. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 34977 in a simple fashion, unfortunately only if 𝑥 and 𝑦 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 34977 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 |
---|---|
wl-sb8mot | ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-sb8et 34954 | . . 3 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)) | |
2 | wl-sb8eut 34978 | . . 3 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | imbi12d 348 | . 2 ⊢ (∀𝑥Ⅎ𝑦𝜑 → ((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑))) |
4 | moeu 2643 | . 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | |
5 | moeu 2643 | . 2 ⊢ (∃*𝑦[𝑦 / 𝑥]𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃!𝑦[𝑦 / 𝑥]𝜑)) | |
6 | 3, 4, 5 | 3bitr4g 317 | 1 ⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1536 ∃wex 1781 Ⅎwnf 1785 [wsb 2069 ∃*wmo 2596 ∃!weu 2628 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 ax-13 2379 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |