This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Relations relsn2
Description: A singleton is a relation iff it has a nonempty domain. (Contributed by NM , 25-Sep-2013) Make hypothesis an antecedent. (Revised by BJ , 12-Feb-2022)
Ref
Expression
Assertion
relsn2 ⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ dom { 𝐴 } ≠ ∅ ) )
Proof
Step
Hyp
Ref
Expression
1
relsng ⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) )
2
dmsnn0 ⊢ ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )
3
1 2
bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ dom { 𝐴 } ≠ ∅ ) )