Metamath Proof Explorer

Theorem ralin

Description: Restricted universal quantification over intersection. (Contributed by Peter Mazsa, 8-Sep-2023)

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

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
2	1	imbi1i	$⊢ (x \in (A \cap B) \to φ) \leftrightarrow ((x \in A \land x \in B) \to φ)$
3		impexp	$⊢ ((x \in A \land x \in B) \to φ) \leftrightarrow (x \in A \to (x \in B \to φ))$
4	2 3	bitri	$⊢ (x \in (A \cap B) \to φ) \leftrightarrow (x \in A \to (x \in B \to φ))$
5	4	ralbii2	$⊢ \forall x \in (A \cap B) φ \leftrightarrow \forall x \in A (x \in B \to φ)$