ralcom4

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019) (Proof shortened by Wolf Lammen, 31-Oct-2024)

		Ref	Expression
	Assertion	ralcom4	$⊢ \forall x \in A \forall y φ \leftrightarrow \forall y \forall x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		19.21v	$⊢ \forall y (x \in A \to φ) \leftrightarrow (x \in A \to \forall y φ)$
2	1	albii	$⊢ \forall x \forall y (x \in A \to φ) \leftrightarrow \forall x (x \in A \to \forall y φ)$
3		alcom	$⊢ \forall y \forall x (x \in A \to φ) \leftrightarrow \forall x \forall y (x \in A \to φ)$
4		df-ral	$⊢ \forall x \in A \forall y φ \leftrightarrow \forall x (x \in A \to \forall y φ)$
5	2 3 4	3bitr4ri	$⊢ \forall x \in A \forall y φ \leftrightarrow \forall y \forall x (x \in A \to φ)$
6		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
7	6	albii	$⊢ \forall y \forall x \in A φ \leftrightarrow \forall y \forall x (x \in A \to φ)$
8	5 7	bitr4i	$⊢ \forall x \in A \forall y φ \leftrightarrow \forall y \forall x \in A φ$

Metamath Proof Explorer

Theorem ralcom4

Proof