This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )