Theorem raltp

Description: Convert a universal quantification over an unordered triple to a conjunction. (Contributed by NM, 13-Sep-2011) (Revised 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	raltp	|- ( A. 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	raltpg	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) ) )
8	1 2 3 7	mp3an	|- ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) )