This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rextpg

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

Ref Expression
Hypotheses ralprg.1 ⊢ x = A → φ ↔ ψ
ralprg.2 ⊢ x = B → φ ↔ χ
raltpg.3 ⊢ x = C → φ ↔ θ
Assertion rextpg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∃ x ∈ A B C φ ↔ ψ ∨ χ ∨ θ

Proof

Step Hyp Ref Expression
1 ralprg.1 ⊢ x = A → φ ↔ ψ
2 ralprg.2 ⊢ x = B → φ ↔ χ
3 raltpg.3 ⊢ x = C → φ ↔ θ
4 1 2 rexprg ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B φ ↔ ψ ∨ χ
5 4 orbi1d ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B φ ∨ ∃ x ∈ C φ ↔ ψ ∨ χ ∨ ∃ x ∈ C φ
6 3 rexsng ⊢ C ∈ X → ∃ x ∈ C φ ↔ θ
7 6 orbi2d ⊢ C ∈ X → ψ ∨ χ ∨ ∃ x ∈ C φ ↔ ψ ∨ χ ∨ θ
8 5 7 sylan9bb ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∃ x ∈ A B φ ∨ ∃ x ∈ C φ ↔ ψ ∨ χ ∨ θ
9 8 3impa ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∃ x ∈ A B φ ∨ ∃ x ∈ C φ ↔ ψ ∨ χ ∨ θ
10 df-tp ⊢ A B C = A B ∪ C
11 10 rexeqi ⊢ ∃ x ∈ A B C φ ↔ ∃ x ∈ A B ∪ C φ
12 rexun ⊢ ∃ x ∈ A B ∪ C φ ↔ ∃ x ∈ A B φ ∨ ∃ x ∈ C φ
13 11 12 bitri ⊢ ∃ x ∈ A B C φ ↔ ∃ x ∈ A B φ ∨ ∃ x ∈ C φ
14 df-3or ⊢ ψ ∨ χ ∨ θ ↔ ψ ∨ χ ∨ θ
15 9 13 14 3bitr4g ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∃ x ∈ A B C φ ↔ ψ ∨ χ ∨ θ