Metamath Proof Explorer


Theorem dfsn2ALT

Description: Alternate definition of singleton, based on the (alternate) definition of pair. Definition 5.1 of TakeutiZaring p. 15. (Contributed by AV, 12-Jun-2022) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion dfsn2ALT { 𝐴 } = { 𝐴 , 𝐴 }

Proof

Step Hyp Ref Expression
1 oridm ( ( 𝑥 = 𝐴𝑥 = 𝐴 ) ↔ 𝑥 = 𝐴 )
2 1 abbii { 𝑥 ∣ ( 𝑥 = 𝐴𝑥 = 𝐴 ) } = { 𝑥𝑥 = 𝐴 }
3 dfpr2 { 𝐴 , 𝐴 } = { 𝑥 ∣ ( 𝑥 = 𝐴𝑥 = 𝐴 ) }
4 df-sn { 𝐴 } = { 𝑥𝑥 = 𝐴 }
5 2 3 4 3eqtr4ri { 𝐴 } = { 𝐴 , 𝐴 }