Theorem rextpg

Description: Convert a restricted existential quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	ralprg.1	|- ( x = A -> ( ph <-> ps ) )
	ralprg.2	|- ( x = B -> ( ph <-> ch ) )
	raltpg.3	|- ( x = C -> ( ph <-> th ) )
Assertion	rextpg	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralprg.1	|- ( x = A -> ( ph <-> ps ) )
2		ralprg.2	|- ( x = B -> ( ph <-> ch ) )
3		raltpg.3	|- ( x = C -> ( ph <-> th ) )
4	1 2	rexprg	|- ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) )
5	4	orbi1d	|- ( ( A e. V /\ B e. W ) -> ( ( E. x e. { A , B } ph \/ E. x e. { C } ph ) <-> ( ( ps \/ ch ) \/ E. x e. { C } ph ) ) )
6	3	rexsng	|- ( C e. X -> ( E. x e. { C } ph <-> th ) )
7	6	orbi2d	|- ( C e. X -> ( ( ( ps \/ ch ) \/ E. x e. { C } ph ) <-> ( ( ps \/ ch ) \/ th ) ) )
8	5 7	sylan9bb	|- ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( ( E. x e. { A , B } ph \/ E. x e. { C } ph ) <-> ( ( ps \/ ch ) \/ th ) ) )
9	8	3impa	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( E. x e. { A , B } ph \/ E. x e. { C } ph ) <-> ( ( ps \/ ch ) \/ th ) ) )
10		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
11	10	rexeqi	|- ( E. x e. { A , B , C } ph <-> E. x e. ( { A , B } u. { C } ) ph )
12		rexun	|- ( E. x e. ( { A , B } u. { C } ) ph <-> ( E. x e. { A , B } ph \/ E. x e. { C } ph ) )
13	11 12	bitri	|- ( E. x e. { A , B , C } ph <-> ( E. x e. { A , B } ph \/ E. x e. { C } ph ) )
14		df-3or	|- ( ( ps \/ ch \/ th ) <-> ( ( ps \/ ch ) \/ th ) )
15	9 13 14	3bitr4g	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) ) )