Description: Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | reuun1 | ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝜑 ∨ 𝜓 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 | ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) | |
2 | orc | ⊢ ( 𝜑 → ( 𝜑 ∨ 𝜓 ) ) | |
3 | 2 | rgenw | ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ( 𝜑 ∨ 𝜓 ) ) |
4 | reuss2 | ⊢ ( ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ( 𝜑 ∨ 𝜓 ) ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝜑 ∨ 𝜓 ) ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) | |
5 | 1 3 4 | mpanl12 | ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝜑 ∨ 𝜓 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 ) |