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	⊢ Ⅎ 𝑦 𝜑
	nfabdw.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		nfabdw.1	⊢ Ⅎ 𝑦 𝜑
2		nfabdw.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3		nfv	⊢ Ⅎ 𝑧 𝜑
4		df-clab	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 )
5		sb6	⊢ ( [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) )
6	4 5	bitri	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜓 } ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) )
7		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 = 𝑧 )
8	7 2	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 = 𝑧 → 𝜓 ) )
9	1 8	nfald	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) )
10	6 9	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 ∈ { 𝑦 ∣ 𝜓 } )
11	3 10	nfcd	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )

Metamath Proof Explorer

Theorem nfabdw

Proof