![]() |
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 uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
Ref | Expression |
---|---|
eubidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
eubidv | ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1992 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | eubidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | eubid 2625 | 1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∃!weu 2607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-12 2196 |
This theorem depends on definitions: df-bi 197 df-ex 1854 df-nf 1859 df-eu 2611 |
This theorem is referenced by: eubii 2629 reueubd 3303 eueq2 3521 eueq3 3522 moeq3 3524 reusv2lem2 5018 reusv2lem2OLD 5019 reusv2lem5 5022 reuhypd 5044 feu 6241 dff3 6536 dff4 6537 omxpenlem 8228 dfac5lem5 9160 dfac5 9161 kmlem2 9185 kmlem12 9195 kmlem13 9196 initoval 16868 termoval 16869 isinito 16871 istermo 16872 initoid 16876 termoid 16877 initoeu1 16882 initoeu2 16887 termoeu1 16889 upxp 21648 edgnbusgreu 26488 nbusgredgeu0 26489 frgrncvvdeqlem2 27475 bnj852 31319 bnj1489 31452 funpartfv 32379 fourierdlem36 40881 eu2ndop1stv 41726 dfdfat2 41735 tz6.12-afv 41777 setrec2lem1 42968 |
Copyright terms: Public domain | W3C validator |