Metamath Proof Explorer

Theorem ralcom3OLD

Description: Obsolete version of ralcom3 as of 22-Dec-2024. (Contributed by NM, 22-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.04	$⊢ (x \in A \to (x \in B \to φ)) \to (x \in B \to (x \in A \to φ))$
2	1	ralimi2	$⊢ \forall x \in A (x \in B \to φ) \to \forall x \in B (x \in A \to φ)$
3		pm2.04	$⊢ (x \in B \to (x \in A \to φ)) \to (x \in A \to (x \in B \to φ))$
4	3	ralimi2	$⊢ \forall x \in B (x \in A \to φ) \to \forall x \in A (x \in B \to φ)$
5	2 4	impbii	$⊢ \forall x \in A (x \in B \to φ) \leftrightarrow \forall x \in B (x \in A \to φ)$