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	$$⊢A\in \mathrm{V}$$
	raltp.2	$$⊢B\in \mathrm{V}$$
	raltp.3	$$⊢C\in \mathrm{V}$$
	raltp.4	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	raltp.5	$$⊢x=B\to \left(\phi \leftrightarrow \chi \right)$$
	raltp.6	$$⊢x=C\to \left(\phi \leftrightarrow \theta \right)$$
Assertion	rextp	$$⊢\exists x\in \left\{A,B,C\right\}\phi \leftrightarrow \left(\psi \vee \chi \vee \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		raltp.1	$$⊢A\in \mathrm{V}$$
2		raltp.2	$$⊢B\in \mathrm{V}$$
3		raltp.3	$$⊢C\in \mathrm{V}$$
4		raltp.4	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
5		raltp.5	$$⊢x=B\to \left(\phi \leftrightarrow \chi \right)$$
6		raltp.6	$$⊢x=C\to \left(\phi \leftrightarrow \theta \right)$$
7	4 5 6	rextpg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(\exists x\in \left\{A,B,C\right\}\phi \leftrightarrow \left(\psi \vee \chi \vee \theta \right)\right)$$
8	1 2 3 7	mp3an	$$⊢\exists x\in \left\{A,B,C\right\}\phi \leftrightarrow \left(\psi \vee \chi \vee \theta \right)$$