nfabdw

Description: Bound-variable hypothesis builder for a class abstraction. Version of nfabd with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) Avoid ax-13 . (Revised by GG, 10-Jan-2024) (Proof shortened by Wolf Lammen, 23-Sep-2024)

	Ref	Expression
Hypotheses	nfabdw.1	$⊢ Ⅎ y φ$
	nfabdw.2	$⊢ φ \to Ⅎ x ψ$
Assertion	nfabdw	$⊢ φ \to \underline{Ⅎ} x \{y \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		nfabdw.1	$⊢ Ⅎ y φ$
2		nfabdw.2	$⊢ φ \to Ⅎ x ψ$
3		nfv	$⊢ Ⅎ z φ$
4		df-clab	$⊢ z \in \{y \| ψ\} \leftrightarrow [z/ y] ψ$
5		sb6	$⊢ [z/ y] ψ \leftrightarrow \forall y (y = z \to ψ)$
6	4 5	bitri	$⊢ z \in \{y \| ψ\} \leftrightarrow \forall y (y = z \to ψ)$
7		nfvd	$⊢ φ \to Ⅎ x y = z$
8	7 2	nfimd	$⊢ φ \to Ⅎ x (y = z \to ψ)$
9	1 8	nfald	$⊢ φ \to Ⅎ x \forall y (y = z \to ψ)$
10	6 9	nfxfrd	$⊢ φ \to Ⅎ x z \in \{y \| ψ\}$
11	3 10	nfcd	$⊢ φ \to \underline{Ⅎ} x \{y \| ψ\}$

Metamath Proof Explorer

Theorem nfabdw

Proof