Theorem rext0

Description: Nonempty existential quantification of a theorem is true. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypothesis	rext0.1	⊢ 𝜑
Assertion	rext0	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		rext0.1	⊢ 𝜑
2	1	notnoti	⊢ ¬ ¬ 𝜑
3	2	ralf0	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ 𝐴 = ∅ )
4	3	notbii	⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ 𝐴 = ∅ )
5		dfrex2	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )
6		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
7	4 5 6	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 ≠ ∅ )