This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A = A A

Proof

Step Hyp Ref Expression
1 oridm ⊢ x = A ∨ x = A ↔ x = A
2 1 abbii ⊢ x | x = A ∨ x = A = x | x = A
3 dfpr2 ⊢ A A = x | x = A ∨ x = A
4 df-sn ⊢ A = x | x = A
5 2 3 4 3eqtr4ri ⊢ A = A A