Theorem ralprg

Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011) (Revised by Mario Carneiro, 23-Apr-2015) Avoid ax-10 , ax-12 . (Revised by Gino Giotto, 30-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ralprg.1	|- ( x = A -> ( ph <-> ps ) )
2		ralprg.2	|- ( x = B -> ( ph <-> ch ) )
3		df-pr	|- { A , B } = ( { A } u. { B } )
4	3	raleqi	|- ( A. x e. { A , B } ph <-> A. x e. ( { A } u. { B } ) ph )
5		ralunb	|- ( A. x e. ( { A } u. { B } ) ph <-> ( A. x e. { A } ph /\ A. x e. { B } ph ) )
6	4 5	bitri	|- ( A. x e. { A , B } ph <-> ( A. x e. { A } ph /\ A. x e. { B } ph ) )
7	1	ralsng	|- ( A e. V -> ( A. x e. { A } ph <-> ps ) )
8	2	ralsng	|- ( B e. W -> ( A. x e. { B } ph <-> ch ) )
9	7 8	bi2anan9	|- ( ( A e. V /\ B e. W ) -> ( ( A. x e. { A } ph /\ A. x e. { B } ph ) <-> ( ps /\ ch ) ) )
10	6 9	bitrid	|- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) )