This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A singleton is a relation iff it is a singleton on an ordered pair.
(Contributed by NM, 24-Sep-2013) (Revised by BJ, 12-Feb-2022)
|
|
Ref |
Expression |
|
Assertion |
relsng |
⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-rel |
⊢ ( Rel { 𝐴 } ↔ { 𝐴 } ⊆ ( V × V ) ) |
| 2 |
|
snssg |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( V × V ) ↔ { 𝐴 } ⊆ ( V × V ) ) ) |
| 3 |
1 2
|
bitr4id |
⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) ) |