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 form). (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 2185 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | exbidh 1859 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∃wex 1771 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfbidf 2216 drex2 2456 rexbida 3315 rexeqf 3396 opabbid 5122 zfrepclf 5189 dfid3 5455 oprabbid 7208 axrepndlem1 10002 axrepndlem2 10003 axrepnd 10004 axpowndlem2 10008 axpowndlem3 10009 axpowndlem4 10010 axregnd 10014 axinfndlem1 10015 axinfnd 10016 axacndlem4 10020 axacndlem5 10021 axacnd 10022 opabdm 30290 opabrn 30291 pm14.122b 40632 pm14.123b 40635 |
Copyright terms: Public domain | W3C validator |