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∈ABCφ↔ψ∨χ∨θ

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∈ABφ↔ψ∨χ
5 4 orbi1d ⊢A∈V∧B∈W→∃x∈ABφ∨∃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∈ABφ∨∃x∈Cφ↔ψ∨χ∨θ
9 8 3impa ⊢A∈V∧B∈W∧C∈X→∃x∈ABφ∨∃x∈Cφ↔ψ∨χ∨θ
10 df-tp ⊢ABC=AB∪C
11 10 rexeqi ⊢∃x∈ABCφ↔∃x∈AB∪Cφ
12 rexun ⊢∃x∈AB∪Cφ↔∃x∈ABφ∨∃x∈Cφ
13 11 12 bitri ⊢∃x∈ABCφ↔∃x∈ABφ∨∃x∈Cφ
14 df-3or ⊢ψ∨χ∨θ↔ψ∨χ∨θ
15 9 13 14 3bitr4g ⊢A∈V∧B∈W∧C∈X→∃x∈ABCφ↔ψ∨χ∨θ