Theorem raldifeq

Description: Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019)

	Ref	Expression
Hypotheses	raldifeq.1	$$⊢\phi \to A\subseteq B$$
	raldifeq.2	$$⊢\phi \to \forall x\in \left(B\setminus A\right)\psi$$
Assertion	raldifeq	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		raldifeq.1	$$⊢\phi \to A\subseteq B$$
2		raldifeq.2	$$⊢\phi \to \forall x\in \left(B\setminus A\right)\psi$$
3	2	biantrud	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \left(\forall x\in A\psi \wedge \forall x\in \left(B\setminus A\right)\psi \right)\right)$$
4		ralunb	$$⊢\forall x\in \left(A\cup \left(B\setminus A\right)\right)\psi \leftrightarrow \left(\forall x\in A\psi \wedge \forall x\in \left(B\setminus A\right)\psi \right)$$
5	3 4	bitr4di	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in \left(A\cup \left(B\setminus A\right)\right)\psi \right)$$
6		undif	$$⊢A\subseteq B\leftrightarrow A\cup \left(B\setminus A\right)=B$$
7	1 6	sylib	$$⊢\phi \to A\cup \left(B\setminus A\right)=B$$
8	7	raleqdv	$$⊢\phi \to \left(\forall x\in \left(A\cup \left(B\setminus A\right)\right)\psi \leftrightarrow \forall x\in B\psi \right)$$
9	5 8	bitrd	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$