Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exbid | Structured version Visualization version GIF version |
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
albid.1 | ⊢ Ⅎ𝑥𝜑 |
albid.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
exbid | ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albid.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nf5ri 2053 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | exbidh 1781 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∃wex 1695 Ⅎwnf 1699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-ex 1696 df-nf 1701 |
This theorem is referenced by: nfbidf 2079 mobid 2477 rexbida 3029 rexeqf 3112 opabbid 4647 zfrepclf 4705 dfid3 4954 oprabbid 6606 axrepndlem1 9293 axrepndlem2 9294 axrepnd 9295 axpowndlem2 9299 axpowndlem3 9300 axpowndlem4 9301 axregnd 9305 axinfndlem1 9306 axinfnd 9307 axacndlem4 9311 axacndlem5 9312 axacnd 9313 opabdm 28803 opabrn 28804 pm14.122b 37646 pm14.123b 37649 |
Copyright terms: Public domain | W3C validator |