Theorem bj-n0i

Description: Inference associated with n0 . Shortens 2ndcdisj (2888>2878), notzfaus (264>253). (Contributed by BJ, 22-Apr-2019)

	Ref	Expression
Hypothesis	bj-n0i.1	⊢ 𝐴 ≠ ∅
Assertion	bj-n0i	⊢ ∃ 𝑥 𝑥 ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		bj-n0i.1	⊢ 𝐴 ≠ ∅
2		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
3	1 2	mpbi	⊢ ∃ 𝑥 𝑥 ∈ 𝐴