Theorem raltpg

Description: Convert a restricted universal quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011) (Revised 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	raltpg	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. 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	ralprg	|- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) )
5	3	ralsng	|- ( C e. X -> ( A. x e. { C } ph <-> th ) )
6	4 5	bi2anan9	|- ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( ( A. x e. { A , B } ph /\ A. x e. { C } ph ) <-> ( ( ps /\ ch ) /\ th ) ) )
7	6	3impa	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A. x e. { A , B } ph /\ A. x e. { C } ph ) <-> ( ( ps /\ ch ) /\ th ) ) )
8		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
9	8	raleqi	|- ( A. x e. { A , B , C } ph <-> A. x e. ( { A , B } u. { C } ) ph )
10		ralunb	|- ( A. x e. ( { A , B } u. { C } ) ph <-> ( A. x e. { A , B } ph /\ A. x e. { C } ph ) )
11	9 10	bitri	|- ( A. x e. { A , B , C } ph <-> ( A. x e. { A , B } ph /\ A. x e. { C } ph ) )
12		df-3an	|- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
13	7 11 12	3bitr4g	|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) ) )