Description: Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrmow when possible. (Contributed by NM, 16-Jun-2017) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfrmo.1 | ⊢ Ⅎ 𝑥 𝐴 | |
| nfrmo.2 | ⊢ Ⅎ 𝑥 𝜑 | ||
| Assertion | nfrmo | ⊢ Ⅎ 𝑥 ∃* 𝑦 ∈ 𝐴 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfrmo.1 | ⊢ Ⅎ 𝑥 𝐴 | |
| 2 | nfrmo.2 | ⊢ Ⅎ 𝑥 𝜑 | |
| 3 | df-rmo | ⊢ ( ∃* 𝑦 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) | |
| 4 | nftru | ⊢ Ⅎ 𝑦 ⊤ | |
| 5 | nfcvf | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ) | |
| 6 | 1 | a1i | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐴 ) |
| 7 | 5 6 | nfeld | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ∈ 𝐴 ) |
| 8 | 2 | a1i | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 ) |
| 9 | 7 8 | nfand | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) |
| 10 | 9 | adantl | ⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) |
| 11 | 4 10 | nfmod2 | ⊢ ( ⊤ → Ⅎ 𝑥 ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) |
| 12 | 11 | mptru | ⊢ Ⅎ 𝑥 ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) |
| 13 | 3 12 | nfxfr | ⊢ Ⅎ 𝑥 ∃* 𝑦 ∈ 𝐴 𝜑 |