wl-dfralflem

Description: Lemma for wl-dfralf and wl-dfralv . (Contributed by Wolf Lammen, 23-May-2023)

		Ref	Expression
	Assertion	wl-dfralflem	$⊢ \forall y \forall x (y \in A \to (x = y \to φ)) \leftrightarrow \forall x (x \in A \to φ)$

Step	Hyp	Ref	Expression
1		alcom	$⊢ \forall y \forall x (y \in A \to (x = y \to φ)) \leftrightarrow \forall x \forall y (y \in A \to (x = y \to φ))$
2		bi2.04	$⊢ (y \in A \to (x = y \to φ)) \leftrightarrow (x = y \to (y \in A \to φ))$
3		equcom	$⊢ x = y \leftrightarrow y = x$
4	3	imbi1i	$⊢ (x = y \to (y \in A \to φ)) \leftrightarrow (y = x \to (y \in A \to φ))$
5	2 4	bitri	$⊢ (y \in A \to (x = y \to φ)) \leftrightarrow (y = x \to (y \in A \to φ))$
6	5	albii	$⊢ \forall y (y \in A \to (x = y \to φ)) \leftrightarrow \forall y (y = x \to (y \in A \to φ))$
7		eleq1w	$⊢ y = x \to (y \in A \leftrightarrow x \in A)$
8	7	imbi1d	$⊢ y = x \to ((y \in A \to φ) \leftrightarrow (x \in A \to φ))$
9	8	equsalvw	$⊢ \forall y (y = x \to (y \in A \to φ)) \leftrightarrow (x \in A \to φ)$
10	6 9	bitri	$⊢ \forall y (y \in A \to (x = y \to φ)) \leftrightarrow (x \in A \to φ)$
11	10	albii	$⊢ \forall x \forall y (y \in A \to (x = y \to φ)) \leftrightarrow \forall x (x \in A \to φ)$
12	1 11	bitri	$⊢ \forall y \forall x (y \in A \to (x = y \to φ)) \leftrightarrow \forall x (x \in A \to φ)$

Metamath Proof Explorer