Metamath Proof Explorer


Theorem rexor

Description: Alias for r19.43 for easier lookup. (Contributed by SN, 5-Jul-2025) (New usage is discouraged.)

Ref Expression
Assertion rexor ⊢ ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 r19.43 ⊢ ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ