Description: Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 19-Feb-2005) (Proof shortened by Andrew Salmon, 9-Jul-2011) (Proof shortened by Wolf Lammen, 24-Dec-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | moanim.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| Assertion | euan | ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃! 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | moanim.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | euex | ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) | |
| 3 | simpl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) | |
| 4 | 1 3 | exlimi | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 ) |
| 5 | 2 4 | syl | ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → 𝜑 ) |
| 6 | ibar | ⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) ) | |
| 7 | 1 6 | eubid | ⊢ ( 𝜑 → ( ∃! 𝑥 𝜓 ↔ ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |
| 8 | 7 | biimprcd | ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → ∃! 𝑥 𝜓 ) ) |
| 9 | 5 8 | jcai | ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ∃! 𝑥 𝜓 ) ) |
| 10 | 7 | biimpa | ⊢ ( ( 𝜑 ∧ ∃! 𝑥 𝜓 ) → ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ) |
| 11 | 9 10 | impbii | ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃! 𝑥 𝜓 ) ) |