Theorem ralidm

Description: Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997)

	Ref	Expression
Assertion	ralidm	$$⊢\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		rzal	$$⊢A=\varnothing \to \forall x\in A\forall x\in A\phi$$
2		rzal	$$⊢A=\varnothing \to \forall x\in A\phi$$
3	1 2	2thd	$$⊢A=\varnothing \to \left(\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\in A\phi \right)$$
4		neq0	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$
5		biimt	$$⊢\exists xx\in A\to \left(\forall x\in A\phi \leftrightarrow \left(\exists xx\in A\to \forall x\in A\phi \right)\right)$$
6		df-ral	$$⊢\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \forall x\in A\phi \right)$$
7		nfra1	$$⊢Ⅎx\forall x\in A\phi$$
8	7	19.23	$$⊢\forall x\left(x\in A\to \forall x\in A\phi \right)\leftrightarrow \left(\exists xx\in A\to \forall x\in A\phi \right)$$
9	6 8	bitri	$$⊢\forall x\in A\forall x\in A\phi \leftrightarrow \left(\exists xx\in A\to \forall x\in A\phi \right)$$
10	5 9	syl6rbbr	$$⊢\exists xx\in A\to \left(\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\in A\phi \right)$$
11	4 10	sylbi	$$⊢\neg A=\varnothing \to \left(\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\in A\phi \right)$$
12	3 11	pm2.61i	$$⊢\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\in A\phi$$