Metamath Proof Explorer

Theorem rextp

Description: Convert an existential quantification over an unordered triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses raltp.1 ⊢ A ∈ V
raltp.2 ⊢ B ∈ V
raltp.3 ⊢ C ∈ V
raltp.4 ⊢ x = A → φ ↔ ψ
raltp.5 ⊢ x = B → φ ↔ χ
raltp.6 ⊢ x = C → φ ↔ θ
Assertion rextp ⊢ ∃ x ∈ A B C φ ↔ ψ ∨ χ ∨ θ

Proof

Step Hyp Ref Expression
1 raltp.1 ⊢ A ∈ V
2 raltp.2 ⊢ B ∈ V
3 raltp.3 ⊢ C ∈ V
4 raltp.4 ⊢ x = A → φ ↔ ψ
5 raltp.5 ⊢ x = B → φ ↔ χ
6 raltp.6 ⊢ x = C → φ ↔ θ
7 4 5 6 rextpg ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ x ∈ A B C φ ↔ ψ ∨ χ ∨ θ
8 1 2 3 7 mp3an ⊢ ∃ x ∈ A B C φ ↔ ψ ∨ χ ∨ θ