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	⊢ 𝐴 ∈ V
	raltp.2	⊢ 𝐵 ∈ V
	raltp.3	⊢ 𝐶 ∈ V
	raltp.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	raltp.5	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
	raltp.6	⊢ ( 𝑥 = 𝐶 → ( 𝜑 ↔ 𝜃 ) )
Assertion	raltp	⊢ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜑 ↔ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		raltp.1	⊢ 𝐴 ∈ V
2		raltp.2	⊢ 𝐵 ∈ V
3		raltp.3	⊢ 𝐶 ∈ V
4		raltp.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5		raltp.5	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
6		raltp.6	⊢ ( 𝑥 = 𝐶 → ( 𝜑 ↔ 𝜃 ) )
7	4 5 6	raltpg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜑 ↔ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) )
8	1 2 3 7	mp3an	⊢ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜑 ↔ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )