Description: Obsolete version of eqsnd as of 3-Jul-2025. (Contributed by Thierry Arnoux, 10-May-2023) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | eqsnd.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = 𝐵 ) | |
| eqsnd.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 ) | ||
| Assertion | eqsndOLD | ⊢ ( 𝜑 → 𝐴 = { 𝐵 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqsnd.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = 𝐵 ) | |
| 2 | eqsnd.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 ) | |
| 3 | simpr | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 ) | |
| 4 | 2 | adantr | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ 𝐴 ) |
| 5 | 3 4 | eqeltrd | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 ) |
| 6 | 1 5 | impbida | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 = 𝐵 ) ) |
| 7 | velsn | ⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 ) | |
| 8 | 6 7 | bitr4di | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝐵 } ) ) |
| 9 | 8 | eqrdv | ⊢ ( 𝜑 → 𝐴 = { 𝐵 } ) |