Theorem ralidm

Description: Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997) Reduce axiom usage. (Revised by GG, 2-Sep-2024)

	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		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)$$
2		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
3		ax-1	$$⊢\forall x\left(x\in A\to \phi \right)\to \left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)$$
4	3	axc4i	$$⊢\forall x\left(x\in A\to \phi \right)\to \forall x\left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)$$
5		pm2.21	$$⊢\neg x\in A\to \left(x\in A\to \phi \right)$$
6		sp	$$⊢\forall x\left(x\in A\to \phi \right)\to \left(x\in A\to \phi \right)$$
7	5 6	ja	$$⊢\left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)\to \left(x\in A\to \phi \right)$$
8	7	alimi	$$⊢\forall x\left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)\to \forall x\left(x\in A\to \phi \right)$$
9	4 8	impbii	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall x\left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)$$
10	2	bicomi	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall x\in A\phi$$
11	10	imbi2i	$$⊢\left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)\leftrightarrow \left(x\in A\to \forall x\in A\phi \right)$$
12	11	albii	$$⊢\forall x\left(x\in A\to \forall x\left(x\in A\to \phi \right)\right)\leftrightarrow \forall x\left(x\in A\to \forall x\in A\phi \right)$$
13	2 9 12	3bitrri	$$⊢\forall x\left(x\in A\to \forall x\in A\phi \right)\leftrightarrow \forall x\in A\phi$$
14	1 13	bitri	$$⊢\forall x\in A\forall x\in A\phi \leftrightarrow \forall x\in A\phi$$