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 \to (φ \leftrightarrow ψ)$
	Assertion	ralidmw	$⊢ \forall x \in A \forall x \in A φ \leftrightarrow \forall x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		ralidmw.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
3	2	imbi2i	$⊢ (x \in A \to \forall x \in A φ) \leftrightarrow (x \in A \to \forall x (x \in A \to φ))$
4	3	albii	$⊢ \forall x (x \in A \to \forall x \in A φ) \leftrightarrow \forall x (x \in A \to \forall x (x \in A \to φ))$
5		pm2.21	$⊢ \neg x \in A \to (x \in A \to φ)$
6		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
7	6 1	imbi12d	$⊢ x = y \to ((x \in A \to φ) \leftrightarrow (y \in A \to ψ))$
8	7	spw	$⊢ \forall x (x \in A \to φ) \to (x \in A \to φ)$
9	5 8	ja	$⊢ (x \in A \to \forall x (x \in A \to φ)) \to (x \in A \to φ)$
10	9	alimi	$⊢ \forall x (x \in A \to \forall x (x \in A \to φ)) \to \forall x (x \in A \to φ)$
11	7	hba1w	$⊢ \forall x (x \in A \to φ) \to \forall x \forall x (x \in A \to φ)$
12		ax-1	$⊢ \forall x (x \in A \to φ) \to (x \in A \to \forall x (x \in A \to φ))$
13	11 12	alrimih	$⊢ \forall x (x \in A \to φ) \to \forall x (x \in A \to \forall x (x \in A \to φ))$
14	10 13	impbii	$⊢ \forall x (x \in A \to \forall x (x \in A \to φ)) \leftrightarrow \forall x (x \in A \to φ)$
15	4 14	bitri	$⊢ \forall x (x \in A \to \forall x \in A φ) \leftrightarrow \forall x (x \in A \to φ)$
16		df-ral	$⊢ \forall x \in A \forall x \in A φ \leftrightarrow \forall x (x \in A \to \forall x \in A φ)$
17	15 16 2	3bitr4i	$⊢ \forall x \in A \forall x \in A φ \leftrightarrow \forall x \in A φ$