Theorem wl-dfrabf

Description: Alternate definition of restricted class abstraction ( df-wl-rab ), when x is not free in A . (Contributed by Wolf Lammen, 29-May-2023)

	Ref	Expression
Assertion	wl-dfrabf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑥 : 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )

Proof

Step	Hyp	Ref	Expression
1		wl-dfrabsb	⊢ { 𝑥 : 𝐴 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) }
2		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
3		id	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝐴 )
4	2 3	wl-clelsb3df	⊢ ( Ⅎ 𝑥 𝐴 → ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
5		clelsb3	⊢ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 )
6	4 5	syl6rbbr	⊢ ( Ⅎ 𝑥 𝐴 → ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ) )
7		sbco2vv	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
8	7	a1i	⊢ ( Ⅎ 𝑥 𝐴 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
9	6 8	anbi12d	⊢ ( Ⅎ 𝑥 𝐴 → ( ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ∧ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
10		df-clab	⊢ ( 𝑧 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) } ↔ [ 𝑧 / 𝑦 ] ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
11		sban	⊢ ( [ 𝑧 / 𝑦 ] ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ∧ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
12	10 11	bitri	⊢ ( 𝑧 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) } ↔ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ∧ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
13		df-clab	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
14		sban	⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
15	13 14	bitri	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
16	9 12 15	3bitr4g	⊢ ( Ⅎ 𝑥 𝐴 → ( 𝑧 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) } ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ) )
17	16	eqrdv	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
18	1 17	syl5eq	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑥 : 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )