Theorem rexrals

Description: If a member of A satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	rexrals	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rals	⊢ ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
2		iba	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
3	2	bicomd	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) )
4	1 3	bitrid	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) )