Metamath Proof Explorer

Theorem rexpr

Description: Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ralpr.1 ⊢ A ∈ V
ralpr.2 ⊢ B ∈ V
ralpr.3 ⊢ x = A → φ ↔ ψ
ralpr.4 ⊢ x = B → φ ↔ χ
Assertion rexpr ⊢ ∃ x ∈ A B φ ↔ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 ralpr.1 ⊢ A ∈ V
2 ralpr.2 ⊢ B ∈ V
3 ralpr.3 ⊢ x = A → φ ↔ ψ
4 ralpr.4 ⊢ x = B → φ ↔ χ
5 3 4 rexprg ⊢ A ∈ V ∧ B ∈ V → ∃ x ∈ A B φ ↔ ψ ∨ χ
6 1 2 5 mp2an ⊢ ∃ x ∈ A B φ ↔ ψ ∨ χ