Metamath Proof Explorer

Theorem raltpg

Description: Convert a restricted universal quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ralprg.1 ⊢ x = A → φ ↔ ψ
ralprg.2 ⊢ x = B → φ ↔ χ
raltpg.3 ⊢ x = C → φ ↔ θ
Assertion raltpg ⊢ 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 ralprg ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ A B φ ↔ ψ ∧ χ
5 3 ralsng ⊢ C ∈ X → ∀ x ∈ C φ ↔ θ
6 4 5 bi2anan9 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∀ x ∈ A B φ ∧ ∀ x ∈ C φ ↔ ψ ∧ χ ∧ θ
7 6 3impa ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∀ x ∈ A B φ ∧ ∀ x ∈ C φ ↔ ψ ∧ χ ∧ θ
8 df-tp ⊢ A B C = A B ∪ C
9 8 raleqi ⊢ ∀ x ∈ A B C φ ↔ ∀ x ∈ A B ∪ C φ
10 ralunb ⊢ ∀ x ∈ A B ∪ C φ ↔ ∀ x ∈ A B φ ∧ ∀ x ∈ C φ
11 9 10 bitri ⊢ ∀ x ∈ A B C φ ↔ ∀ x ∈ A B φ ∧ ∀ x ∈ C φ
12 df-3an ⊢ ψ ∧ χ ∧ θ ↔ ψ ∧ χ ∧ θ
13 7 11 12 3bitr4g ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∀ x ∈ A B C φ ↔ ψ ∧ χ ∧ θ