![]() |
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 2183 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | exbidh 1862 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∃wex 1773 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 |
This theorem is referenced by: nfbidf 2212 drex2 2435 rexbida 3259 rexeqfOLD 3338 opabbid 5214 zfrepclf 5295 dfid3 5579 oprabbid 7485 axrepndlem1 10622 axrepndlem2 10623 axrepnd 10624 axpowndlem2 10628 axpowndlem3 10629 axpowndlem4 10630 axregnd 10634 axinfndlem1 10635 axinfnd 10636 axacndlem4 10640 axacndlem5 10641 axacnd 10642 opabdm 32500 opabrn 32501 pm14.122b 44007 pm14.123b 44010 |
Copyright terms: Public domain | W3C validator |