Theorem n0rex

Description: There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020)

	Ref	Expression
Assertion	n0rex	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
2	1	ancli	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
3	2	eximi	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
4		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
5		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
6	3 4 5	3imtr4i	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 )