Theorem 2ralsng

Description: Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ralsng.1	|- ( x = A -> ( ph <-> ps ) )
2		2ralsng.1	|- ( y = B -> ( ps <-> ch ) )
3	1	ralbidv	|- ( x = A -> ( A. y e. { B } ph <-> A. y e. { B } ps ) )
4	3	ralsng	|- ( A e. V -> ( A. x e. { A } A. y e. { B } ph <-> A. y e. { B } ps ) )
5	2	ralsng	|- ( B e. W -> ( A. y e. { B } ps <-> ch ) )
6	4 5	sylan9bb	|- ( ( A e. V /\ B e. W ) -> ( A. x e. { A } A. y e. { B } ph <-> ch ) )