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

Metamath Proof Explorer

Theorem ralcom3

Description: A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004) (Proof shortened by Wolf Lammen, 22-Dec-2024)

		Ref	Expression
	Assertion	ralcom3	$⊢ \forall x \in A (x \in B \to φ) \leftrightarrow \forall x \in B (x \in A \to φ)$

Proof

Step	Hyp	Ref	Expression
1		bi2.04	$⊢ (x \in A \to (x \in B \to φ)) \leftrightarrow (x \in B \to (x \in A \to φ))$
2	1	ralbii2	$⊢ \forall x \in A (x \in B \to φ) \leftrightarrow \forall x \in B (x \in A \to φ)$