Metamath Proof Explorer

Theorem rexdifi

Description: Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023)

		Ref	Expression
	Assertion	rexdifi	$⊢ (\exists x \in A φ \land \forall x \in B \neg φ) \to \exists x \in (A ∖ B) φ$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
2		df-ral	$⊢ \forall x \in B \neg φ \leftrightarrow \forall x (x \in B \to \neg φ)$
3		nfa1	$⊢ Ⅎ x \forall x (x \in B \to \neg φ)$
4		simprl	$⊢ (\forall x (x \in B \to \neg φ) \land (x \in A \land φ)) \to x \in A$
5		con2	$⊢ (x \in B \to \neg φ) \to (φ \to \neg x \in B)$
6	5	sps	$⊢ \forall x (x \in B \to \neg φ) \to (φ \to \neg x \in B)$
7	6	com12	$⊢ φ \to (\forall x (x \in B \to \neg φ) \to \neg x \in B)$
8	7	adantl	$⊢ (x \in A \land φ) \to (\forall x (x \in B \to \neg φ) \to \neg x \in B)$
9	8	impcom	$⊢ (\forall x (x \in B \to \neg φ) \land (x \in A \land φ)) \to \neg x \in B$
10	4 9	eldifd	$⊢ (\forall x (x \in B \to \neg φ) \land (x \in A \land φ)) \to x \in (A ∖ B)$
11		simprr	$⊢ (\forall x (x \in B \to \neg φ) \land (x \in A \land φ)) \to φ$
12	10 11	jca	$⊢ (\forall x (x \in B \to \neg φ) \land (x \in A \land φ)) \to (x \in (A ∖ B) \land φ)$
13	12	ex	$⊢ \forall x (x \in B \to \neg φ) \to ((x \in A \land φ) \to (x \in (A ∖ B) \land φ))$
14	3 13	eximd	$⊢ \forall x (x \in B \to \neg φ) \to (\exists x (x \in A \land φ) \to \exists x (x \in (A ∖ B) \land φ))$
15	14	impcom	$⊢ (\exists x (x \in A \land φ) \land \forall x (x \in B \to \neg φ)) \to \exists x (x \in (A ∖ B) \land φ)$
16	1 2 15	syl2anb	$⊢ (\exists x \in A φ \land \forall x \in B \neg φ) \to \exists x (x \in (A ∖ B) \land φ)$
17		df-rex	$⊢ \exists x \in (A ∖ B) φ \leftrightarrow \exists x (x \in (A ∖ B) \land φ)$
18	16 17	sylibr	$⊢ (\exists x \in A φ \land \forall x \in B \neg φ) \to \exists x \in (A ∖ B) φ$