Theorem ralpr

Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007) (Revised by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	ralpr.1	|- A e. _V
	ralpr.2	|- B e. _V
	ralpr.3	|- ( x = A -> ( ph <-> ps ) )
	ralpr.4	|- ( x = B -> ( ph <-> ch ) )
Assertion	ralpr	|- ( A. x e. { A , B } ph <-> ( ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralpr.1	|- A e. _V
2		ralpr.2	|- B e. _V
3		ralpr.3	|- ( x = A -> ( ph <-> ps ) )
4		ralpr.4	|- ( x = B -> ( ph <-> ch ) )
5	3 4	ralprg	|- ( ( A e. _V /\ B e. _V ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) )
6	1 2 5	mp2an	|- ( A. x e. { A , B } ph <-> ( ps /\ ch ) )