Metamath Proof Explorer

Theorem raltp

Description: Convert a universal quantification over an unordered triple to a conjunction. (Contributed by NM, 13-Sep-2011) (Revised 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 raltp ⊢∀x∈ABCφ↔ψ∧χ∧θ

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 raltpg ⊢A∈V∧B∈V∧C∈V→∀x∈ABCφ↔ψ∧χ∧θ
8 1 2 3 7 mp3an ⊢∀x∈ABCφ↔ψ∧χ∧θ