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\to \left(\phi \leftrightarrow \psi \right)$$
	2ralsng.1	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	2ralsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall x\in \left\{A\right\}\forall y\in \left\{B\right\}\phi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralsng.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		2ralsng.1	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
3	1	ralbidv	$$⊢x=A\to \left(\forall y\in \left\{B\right\}\phi \leftrightarrow \forall y\in \left\{B\right\}\psi \right)$$
4	3	ralsng	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\forall y\in \left\{B\right\}\phi \leftrightarrow \forall y\in \left\{B\right\}\psi \right)$$
5	2	ralsng	$$⊢B\in W\to \left(\forall y\in \left\{B\right\}\psi \leftrightarrow \chi \right)$$
6	4 5	sylan9bb	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall x\in \left\{A\right\}\forall y\in \left\{B\right\}\phi \leftrightarrow \chi \right)$$