| 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 1927 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
| 3 | mobi 2547 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | |
| 4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∃*wmo 2538 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-mo 2540 |
| This theorem is referenced by: moanimv 2619 rmobidva 3395 rmoeq1OLD 3418 mosubopt 5515 dffun6f 6579 funmo 6581 funmoOLD 6582 caovmo 7670 1stconst 8125 2ndconst 8126 brdom3 10568 brdom6disj 10572 imasaddfnlem 17573 imasvscafn 17582 hausflim 23989 hausflf 24005 cnextfun 24072 haustsms 24144 limcmo 25917 perfdvf 25938 rmounid 32514 rmoeqbidv 36214 disjeq12dv 36216 phpreu 37611 alrmomodm 38360 funressnfv 47055 funressnmo 47058 mosn 48732 mof02 48748 mofsn2 48754 f1omo 48792 isthinc 49069 isthincd2lem1 49075 thincmoALT 49078 thincmod 49079 isthincd 49085 thincpropd 49091 setcthin 49112 |
| Copyright terms: Public domain | W3C validator |