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 1843 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | eubidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | eubid 2488 | 1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∃!weu 2470 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 df-eu 2474 |
This theorem is referenced by: eubii 2492 reueubd 3164 eueq2 3380 eueq3 3381 moeq3 3383 reusv2lem2 4869 reusv2lem2OLD 4870 reusv2lem5 4873 reuhypd 4895 feu 6080 dff3 6372 dff4 6373 omxpenlem 8061 dfac5lem5 8950 dfac5 8951 kmlem2 8973 kmlem12 8983 kmlem13 8984 initoval 16647 termoval 16648 isinito 16650 istermo 16651 initoid 16655 termoid 16656 initoeu1 16661 initoeu2 16666 termoeu1 16668 upxp 21426 edgnbusgreu 26269 frgrncvvdeqlem2 27164 bnj852 30991 bnj1489 31124 funpartfv 32052 fourierdlem36 40360 eu2ndop1stv 41202 dfdfat2 41211 tz6.12-afv 41253 setrec2lem1 42440 |
Copyright terms: Public domain | W3C validator |