![]() |
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 2193 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | exbidh 1868 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfbidf 2224 drex2 2453 rexbida 3277 rexeqf 3351 opabbid 5095 zfrepclf 5162 dfid3 5427 oprabbid 7198 axrepndlem1 10003 axrepndlem2 10004 axrepnd 10005 axpowndlem2 10009 axpowndlem3 10010 axpowndlem4 10011 axregnd 10015 axinfndlem1 10016 axinfnd 10017 axacndlem4 10021 axacndlem5 10022 axacnd 10023 opabdm 30375 opabrn 30376 pm14.122b 41127 pm14.123b 41130 |
Copyright terms: Public domain | W3C validator |