![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eubidv | Structured version Visualization version GIF version |
Description: Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.) |
Ref | Expression |
---|---|
eubidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
eubidv | ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eubidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | alrimiv 1930 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
3 | eubi 2577 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 ∃!weu 2561 |
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 2533 df-eu 2562 |
This theorem is referenced by: euorv 2607 euanv 2619 reubidva 3391 reueubd 3394 reueq1OLD 3416 eueq2 3702 eueq3 3703 moeq3 3704 reusv2lem2 5390 reusv2lem5 5393 reuhypd 5410 feu 6754 dff3 7086 dff4 7087 omxpenlem 9056 dfac5lem5 10104 dfac5 10105 kmlem2 10128 kmlem12 10138 kmlem13 10139 initoval 17925 termoval 17926 isinito 17928 istermo 17929 initoid 17933 termoid 17934 initoeu1 17943 initoeu2 17948 termoeu1 17950 upxp 23056 edgnbusgreu 28489 nbusgredgeu0 28490 frgrncvvdeqlem2 29418 bnj852 33763 bnj1489 33898 funpartfv 34747 fsuppind 40951 fourierdlem36 44632 aiotaval 45575 eu2ndop1stv 45605 dfdfat2 45608 tz6.12-afv 45653 tz6.12-afv2 45720 dfatcolem 45735 prprsprreu 45959 prprreueq 45960 setrec2lem1 47386 |
Copyright terms: Public domain | W3C validator |