Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . (Contributed by NM, 14-Nov-2004) (Revised by NM, 16-Jun-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | reuxfr.1 | ⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 ) | |
| reuxfr.2 | ⊢ ( 𝑥 ∈ 𝐵 → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) | ||
| Assertion | reuxfr | ⊢ ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reuxfr.1 | ⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 ) | |
| 2 | reuxfr.2 | ⊢ ( 𝑥 ∈ 𝐵 → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) | |
| 3 | 1 | adantl | ⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 ) |
| 4 | 2 | adantl | ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) |
| 5 | 3 4 | reuxfrd | ⊢ ( ⊤ → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜑 ) ) |
| 6 | 5 | mptru | ⊢ ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜑 ) |