|   | 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 2194 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | 
| 3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 4 | 2, 3 | exbidh 1866 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∃wex 1778 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: nfbidf 2223 drex2 2446 rexbida 3271 rexeqfOLD 3354 opabbid 5207 zfrepclf 5290 dfid3 5580 oprabbid 7499 axrepndlem1 10633 axrepndlem2 10634 axrepnd 10635 axpowndlem2 10639 axpowndlem3 10640 axpowndlem4 10641 axregnd 10645 axinfndlem1 10646 axinfnd 10647 axacndlem4 10651 axacndlem5 10652 axacnd 10653 opabdm 32624 opabrn 32625 pm14.122b 44447 pm14.123b 44450 modelaxreplem3 45002 | 
| Copyright terms: Public domain | W3C validator |