Metamath Proof Explorer

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 ⊢ ∃ x ∈ A φ → ∀∃ x ∈ A φ → ψ ↔ ∀ x ∈ A φ → ψ

Proof

Step Hyp Ref Expression
1 df-rals ⊢ ∀∃ x ∈ A φ → ψ ↔ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ
2 iba ⊢ ∃ x ∈ A φ → ∀ x ∈ A φ → ψ ↔ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ
3 2 bicomd ⊢ ∃ x ∈ A φ → ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ↔ ∀ x ∈ A φ → ψ
4 1 3 bitrid ⊢ ∃ x ∈ A φ → ∀∃ x ∈ A φ → ψ ↔ ∀ x ∈ A φ → ψ