| 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 1927 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
| 3 | eubi 2584 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | |
| 4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∃!weu 2568 |
| 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 df-eu 2569 |
| This theorem is referenced by: euorv 2612 euanv 2624 reubidva 3396 reueubd 3399 reueq1OLD 3419 reueqbidv 3423 eueq2 3716 eueq3 3717 moeq3 3718 reusv2lem2 5399 reusv2lem5 5402 reuhypd 5419 feu 6784 dff3 7120 dff4 7121 omxpenlem 9113 dfac5lem5 10167 dfac5 10169 kmlem2 10192 kmlem12 10202 kmlem13 10203 initoval 18038 termoval 18039 isinito 18041 istermo 18042 initoid 18046 termoid 18047 initoeu1 18056 initoeu2 18061 termoeu1 18063 upxp 23631 edgnbusgreu 29384 nbusgredgeu0 29385 frgrncvvdeqlem2 30319 bnj852 34935 bnj1489 35070 funpartfv 35946 fsuppind 42600 wfac8prim 45019 fourierdlem36 46158 aiotaval 47107 eu2ndop1stv 47137 dfdfat2 47140 tz6.12-afv 47185 tz6.12-afv2 47252 dfatcolem 47267 prprsprreu 47506 prprreueq 47507 termcterm 49145 termc2 49148 setrec2lem1 49212 |
| Copyright terms: Public domain | W3C validator |