Theorem ralrals

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

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

Proof

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