Description: Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . See nfmodv for a version replacing the distinctor with a disjoint variable condition, not requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) Avoid df-eu . (Revised by BJ, 14-Oct-2022) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfmod2.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| nfmod2.2 | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 ) | ||
| Assertion | nfmod2 | ⊢ ( 𝜑 → Ⅎ 𝑥 ∃* 𝑦 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfmod2.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| 2 | nfmod2.2 | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 ) | |
| 3 | df-mo | ⊢ ( ∃* 𝑦 𝜓 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) | |
| 4 | nfv | ⊢ Ⅎ 𝑧 𝜑 | |
| 5 | nfeqf1 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 = 𝑧 ) | |
| 6 | 5 | adantl | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 = 𝑧 ) |
| 7 | 2 6 | nfimd | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 8 | 1 7 | nfald2 | ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 9 | 4 8 | nfexd | ⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 10 | 3 9 | nfxfrd | ⊢ ( 𝜑 → Ⅎ 𝑥 ∃* 𝑦 𝜓 ) |