Description: If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when A is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fnsnr | ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝐵 ∈ 𝐹 → 𝐵 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fnresdm | ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝐹 ↾ { 𝐴 } ) = 𝐹 ) | |
| 2 | fnfun | ⊢ ( 𝐹 Fn { 𝐴 } → Fun 𝐹 ) | |
| 3 | funressn | ⊢ ( Fun 𝐹 → ( 𝐹 ↾ { 𝐴 } ) ⊆ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) | |
| 4 | 2 3 | syl | ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝐹 ↾ { 𝐴 } ) ⊆ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) |
| 5 | 1 4 | eqsstrrd | ⊢ ( 𝐹 Fn { 𝐴 } → 𝐹 ⊆ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) |
| 6 | 5 | sseld | ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝐵 ∈ 𝐹 → 𝐵 ∈ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) ) |
| 7 | elsni | ⊢ ( 𝐵 ∈ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → 𝐵 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) | |
| 8 | 6 7 | syl6 | ⊢ ( 𝐹 Fn { 𝐴 } → ( 𝐵 ∈ 𝐹 → 𝐵 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) ) |