![]() |
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 2236 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | exbidh 1968 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∃wex 1878 Ⅎwnf 1882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-12 2220 |
This theorem depends on definitions: df-bi 199 df-ex 1879 df-nf 1883 |
This theorem is referenced by: nfbidf 2267 drex2 2463 eubidOLD 2661 mobidOLDOLD 2681 rexbida 3257 rexeqf 3347 opabbid 4940 zfrepclf 5003 dfid3 5253 oprabbid 6973 axrepndlem1 9736 axrepndlem2 9737 axrepnd 9738 axpowndlem2 9742 axpowndlem3 9743 axpowndlem4 9744 axregnd 9748 axinfndlem1 9749 axinfnd 9750 axacndlem4 9754 axacndlem5 9755 axacnd 9756 opabdm 29966 opabrn 29967 pm14.122b 39462 pm14.123b 39465 |
Copyright terms: Public domain | W3C validator |