Metamath Proof Explorer

Theorem raldifb

Description: Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		impexp	$⊢ ((x \in A \land x \notin B) \to φ) \leftrightarrow (x \in A \to (x \notin B \to φ))$
2		df-nel	$⊢ x \notin B \leftrightarrow \neg x \in B$
3	2	anbi2i	$⊢ (x \in A \land x \notin B) \leftrightarrow (x \in A \land \neg x \in B)$
4		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
5	3 4	bitr4i	$⊢ (x \in A \land x \notin B) \leftrightarrow x \in (A ∖ B)$
6	5	imbi1i	$⊢ ((x \in A \land x \notin B) \to φ) \leftrightarrow (x \in (A ∖ B) \to φ)$
7	1 6	bitr3i	$⊢ (x \in A \to (x \notin B \to φ)) \leftrightarrow (x \in (A ∖ B) \to φ)$
8	7	ralbii2	$⊢ \forall x \in A (x \notin B \to φ) \leftrightarrow \forall x \in (A ∖ B) φ$