Theorem ralidmw

Description: Idempotent law for restricted quantifier. Weak version of ralidm , which does not require ax-10 , ax-12 , but requires ax-8 . (Contributed by GG, 30-Sep-2024)

	Ref	Expression
Hypothesis	ralidmw.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	ralidmw	|- ( A. x e. A A. x e. A ph <-> A. x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		ralidmw.1	|- ( x = y -> ( ph <-> ps ) )
2		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
3	2	imbi2i	|- ( ( x e. A -> A. x e. A ph ) <-> ( x e. A -> A. x ( x e. A -> ph ) ) )
4	3	albii	|- ( A. x ( x e. A -> A. x e. A ph ) <-> A. x ( x e. A -> A. x ( x e. A -> ph ) ) )
5		pm2.21	|- ( -. x e. A -> ( x e. A -> ph ) )
6		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
7	6 1	imbi12d	|- ( x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ps ) ) )
8	7	spw	|- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
9	5 8	ja	|- ( ( x e. A -> A. x ( x e. A -> ph ) ) -> ( x e. A -> ph ) )
10	9	alimi	|- ( A. x ( x e. A -> A. x ( x e. A -> ph ) ) -> A. x ( x e. A -> ph ) )
11	7	hba1w	|- ( A. x ( x e. A -> ph ) -> A. x A. x ( x e. A -> ph ) )
12		ax-1	|- ( A. x ( x e. A -> ph ) -> ( x e. A -> A. x ( x e. A -> ph ) ) )
13	11 12	alrimih	|- ( A. x ( x e. A -> ph ) -> A. x ( x e. A -> A. x ( x e. A -> ph ) ) )
14	10 13	impbii	|- ( A. x ( x e. A -> A. x ( x e. A -> ph ) ) <-> A. x ( x e. A -> ph ) )
15	4 14	bitri	|- ( A. x ( x e. A -> A. x e. A ph ) <-> A. x ( x e. A -> ph ) )
16		df-ral	|- ( A. x e. A A. x e. A ph <-> A. x ( x e. A -> A. x e. A ph ) )
17	15 16 2	3bitr4i	|- ( A. x e. A A. x e. A ph <-> A. x e. A ph )