Theorem 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) (Revised by Gino Giotto, 10-Jan-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	1 2	alrimi	⊢ ( 𝜑 → ∀ 𝑦 Ⅎ 𝑥 𝜓 )
6		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 Ⅎ 𝑥 𝜓
7		sb6	⊢ ( [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) )
8	7	a1i	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → ( [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) ) )
9	7	biimpri	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) → [ 𝑧 / 𝑦 ] 𝜓 )
10	9	axc4i	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜓 ) → ∀ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 )
11	8 10	syl6bi	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → ( [ 𝑧 / 𝑦 ] 𝜓 → ∀ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 ) )
12	6 11	nf5d	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 )
13	6 12	nfim1	⊢ Ⅎ 𝑦 ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 )
14		sbequ12	⊢ ( 𝑦 = 𝑧 → ( 𝜓 ↔ [ 𝑧 / 𝑦 ] 𝜓 ) )
15	14	imbi2d	⊢ ( 𝑦 = 𝑧 → ( ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → 𝜓 ) ↔ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ) )
16	13 15	equsalv	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑧 → ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → 𝜓 ) ) ↔ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) )
17	16	bicomi	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → 𝜓 ) ) )
18		nfv	⊢ Ⅎ 𝑥 𝑦 = 𝑧
19		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜓
20	19	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 Ⅎ 𝑥 𝜓
21		sp	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 𝜓 )
22	20 21	nfim1	⊢ Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → 𝜓 )
23	18 22	nfim	⊢ Ⅎ 𝑥 ( 𝑦 = 𝑧 → ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → 𝜓 ) )
24	23	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑧 → ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → 𝜓 ) )
25	17 24	nfxfr	⊢ Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 )
26		pm5.5	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → ( ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ↔ [ 𝑧 / 𝑦 ] 𝜓 ) )
27	20 26	nfbidf	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → ( Ⅎ 𝑥 ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → [ 𝑧 / 𝑦 ] 𝜓 ) ↔ Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 ) )
28	25 27	mpbii	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 )
29	5 28	syl	⊢ ( 𝜑 → Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 )
30	4 29	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 ∈ { 𝑦 ∣ 𝜓 } )
31	3 30	nfcd	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )