Theorem exsnrex

Description: There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018)

	Ref	Expression
Assertion	exsnrex	⊢ ( ∃ 𝑥 𝑀 = { 𝑥 } ↔ ∃ 𝑥 ∈ 𝑀 𝑀 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		vsnid	⊢ 𝑥 ∈ { 𝑥 }
2		eleq2	⊢ ( 𝑀 = { 𝑥 } → ( 𝑥 ∈ 𝑀 ↔ 𝑥 ∈ { 𝑥 } ) )
3	1 2	mpbiri	⊢ ( 𝑀 = { 𝑥 } → 𝑥 ∈ 𝑀 )
4	3	pm4.71ri	⊢ ( 𝑀 = { 𝑥 } ↔ ( 𝑥 ∈ 𝑀 ∧ 𝑀 = { 𝑥 } ) )
5	4	exbii	⊢ ( ∃ 𝑥 𝑀 = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑀 ∧ 𝑀 = { 𝑥 } ) )
6		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑀 𝑀 = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑀 ∧ 𝑀 = { 𝑥 } ) )
7	5 6	bitr4i	⊢ ( ∃ 𝑥 𝑀 = { 𝑥 } ↔ ∃ 𝑥 ∈ 𝑀 𝑀 = { 𝑥 } )