Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Use reuhyp to eliminate the second hypothesis. (Contributed by NM, 14-Nov-2004)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | reuxfr1.1 | ⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 ) | |
| reuxfr1.2 | ⊢ ( 𝑥 ∈ 𝐵 → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) | ||
| reuxfr1.3 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | reuxfr1 | ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reuxfr1.1 | ⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 ) | |
| 2 | reuxfr1.2 | ⊢ ( 𝑥 ∈ 𝐵 → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) | |
| 3 | reuxfr1.3 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 4 | 1 | adantl | ⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 ) |
| 5 | 2 | adantl | ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) |
| 6 | 4 5 3 | reuxfr1ds | ⊢ ( ⊤ → ( ∃! 𝑥 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) ) |
| 7 | 6 | mptru | ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) |