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 e. _V
	raltp.2	|- B e. _V
	raltp.3	|- C e. _V
	raltp.4	|- ( x = A -> ( ph <-> ps ) )
	raltp.5	|- ( x = B -> ( ph <-> ch ) )
	raltp.6	|- ( x = C -> ( ph <-> th ) )
Assertion	rextp	|- ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) )

Proof

Step	Hyp	Ref	Expression
1		raltp.1	|- A e. _V
2		raltp.2	|- B e. _V
3		raltp.3	|- C e. _V
4		raltp.4	|- ( x = A -> ( ph <-> ps ) )
5		raltp.5	|- ( x = B -> ( ph <-> ch ) )
6		raltp.6	|- ( x = C -> ( ph <-> th ) )
7	4 5 6	rextpg	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) ) )
8	1 2 3 7	mp3an	|- ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) )