![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mobidv | Structured version Visualization version GIF version |
Description: Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.) |
Ref | Expression |
---|---|
mobidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
mobidv | ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mobidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | alrimiv 1970 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
3 | mobi 2560 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1599 ∃*wmo 2549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-mo 2551 |
This theorem is referenced by: moanimv 2654 rmoeq1 3333 mosubopt 5207 dffun6f 6149 funmo 6151 caovmo 7148 1stconst 7546 2ndconst 7547 brdom3 9685 brdom6disj 9689 imasaddfnlem 16574 imasvscafn 16583 hausflim 22193 hausflf 22209 cnextfun 22276 haustsms 22347 limcmo 24083 perfdvf 24104 phpreu 34018 alrmomodm 34752 funressnfv 42107 funressnmo 42111 |
Copyright terms: Public domain | W3C validator |