Metamath Proof Explorer

Theorem wl-dfrexsb

Description: An alternate definition of restricted existential quantification ( df-wl-rex ) using substitution. (Contributed by Wolf Lammen, 25-May-2023)

		Ref	Expression
	Assertion	wl-dfrexsb	$⊢ \exists x : A φ \leftrightarrow \exists y (y \in A \land [y/ x] φ)$

Proof

Step	Hyp	Ref	Expression
1		df-wl-rex	$⊢ \exists x : A φ \leftrightarrow \neg \forall x : A \neg φ$
2		wl-dfralsb	$⊢ \forall x : A \neg φ \leftrightarrow \forall y (y \in A \to [y/ x] \neg φ)$
3	1 2	xchbinx	$⊢ \exists x : A φ \leftrightarrow \neg \forall y (y \in A \to [y/ x] \neg φ)$
4		sbn	$⊢ [y/ x] \neg φ \leftrightarrow \neg [y/ x] φ$
5	4	imbi2i	$⊢ (y \in A \to [y/ x] \neg φ) \leftrightarrow (y \in A \to \neg [y/ x] φ)$
6	5	albii	$⊢ \forall y (y \in A \to [y/ x] \neg φ) \leftrightarrow \forall y (y \in A \to \neg [y/ x] φ)$
7		imnang	$⊢ \forall y (y \in A \to \neg [y/ x] φ) \leftrightarrow \forall y \neg (y \in A \land [y/ x] φ)$
8		alnex	$⊢ \forall y \neg (y \in A \land [y/ x] φ) \leftrightarrow \neg \exists y (y \in A \land [y/ x] φ)$
9	6 7 8	3bitri	$⊢ \forall y (y \in A \to [y/ x] \neg φ) \leftrightarrow \neg \exists y (y \in A \land [y/ x] φ)$
10	9	con2bii	$⊢ \exists y (y \in A \land [y/ x] φ) \leftrightarrow \neg \forall y (y \in A \to [y/ x] \neg φ)$
11	3 10	bitr4i	$⊢ \exists x : A φ \leftrightarrow \exists y (y \in A \land [y/ x] φ)$