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 ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 r19.43 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )