Theorem ralbinrald

Description: Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017)

	Ref	Expression
Hypotheses	ralbinrald.1	$$⊢\phi \to X\in A$$
	ralbinrald.2	$$⊢x\in A\to x=X$$
	ralbinrald.3	$$⊢x=X\to \left(\psi \leftrightarrow \theta \right)$$
Assertion	ralbinrald	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralbinrald.1	$$⊢\phi \to X\in A$$
2		ralbinrald.2	$$⊢x\in A\to x=X$$
3		ralbinrald.3	$$⊢x=X\to \left(\psi \leftrightarrow \theta \right)$$
4	3	adantl	$$⊢\left(\phi \wedge x=X\right)\to \left(\psi \leftrightarrow \theta \right)$$
5	1 4	rspcdv	$$⊢\phi \to \left(\forall x\in A\psi \to \theta \right)$$
6	3	bicomd	$$⊢x=X\to \left(\theta \leftrightarrow \psi \right)$$
7	2 6	syl	$$⊢x\in A\to \left(\theta \leftrightarrow \psi \right)$$
8	7	adantl	$$⊢\left(\phi \wedge x\in A\right)\to \left(\theta \leftrightarrow \psi \right)$$
9	8	biimpd	$$⊢\left(\phi \wedge x\in A\right)\to \left(\theta \to \psi \right)$$
10	9	ralrimdva	$$⊢\phi \to \left(\theta \to \forall x\in A\psi \right)$$
11	5 10	impbid	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \theta \right)$$