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

Proof

Step	Hyp	Ref	Expression
1		ralprg.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		ralprg.2	$$⊢x=B\to \left(\phi \leftrightarrow \chi \right)$$
3		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
4	3	raleqi	$$⊢\forall x\in \left\{A,B\right\}\phi \leftrightarrow \forall x\in \left(\left\{A\right\}\cup \left\{B\right\}\right)\phi$$
5		ralunb	$$⊢\forall x\in \left(\left\{A\right\}\cup \left\{B\right\}\right)\phi \leftrightarrow \left(\forall x\in \left\{A\right\}\phi \wedge \forall x\in \left\{B\right\}\phi \right)$$
6	4 5	bitri	$$⊢\forall x\in \left\{A,B\right\}\phi \leftrightarrow \left(\forall x\in \left\{A\right\}\phi \wedge \forall x\in \left\{B\right\}\phi \right)$$
7	1	ralsng	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \psi \right)$$
8	2	ralsng	$$⊢B\in W\to \left(\forall x\in \left\{B\right\}\phi \leftrightarrow \chi \right)$$
9	7 8	bi2anan9	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left(\forall x\in \left\{A\right\}\phi \wedge \forall x\in \left\{B\right\}\phi \right)\leftrightarrow \left(\psi \wedge \chi \right)\right)$$
10	6 9	bitrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall x\in \left\{A,B\right\}\phi \leftrightarrow \left(\psi \wedge \chi \right)\right)$$