![]() |
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 1930 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
3 | mobi 2541 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 ∃*wmo 2532 |
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 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-mo 2534 |
This theorem is referenced by: moanimv 2615 rmobidva 3391 rmoeq1OLD 3416 mosubopt 5509 dffun6f 6558 funmo 6560 funmoOLD 6561 caovmo 7640 1stconst 8082 2ndconst 8083 brdom3 10519 brdom6disj 10523 imasaddfnlem 17470 imasvscafn 17479 hausflim 23476 hausflf 23492 cnextfun 23559 haustsms 23631 limcmo 25390 perfdvf 25411 rmounid 31722 phpreu 36460 alrmomodm 37216 funressnfv 45739 funressnmo 45742 mosn 47450 mof02 47458 mofsn2 47464 f1omo 47480 isthinc 47594 isthincd2lem1 47600 thincmoALT 47603 thincmod 47604 isthincd 47610 setcthin 47628 |
Copyright terms: Public domain | W3C validator |