Theorem r19.9rzv

Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998)

	Ref	Expression
Assertion	r19.9rzv	⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		dfrex2	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )
2		r19.3rzv	⊢ ( 𝐴 ≠ ∅ → ( ¬ 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) )
3	2	con1bid	⊢ ( 𝐴 ≠ ∅ → ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ 𝜑 ) )
4	1 3	bitr2id	⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 ) )