Theorem rextp

Description: Convert an existential quantification over an unordered triple to a disjunction. (Contributed 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	rextp	⊢ ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜑 ↔ ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) )

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	rextpg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜑 ↔ ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) ) )
8	1 2 3 7	mp3an	⊢ ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝜑 ↔ ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) )