Theorem wl-dfclab

Description: Rederive df-clab from wl-clabv . (Contributed by Wolf Lammen, 31-May-2023) (Proof modification is discouraged.)

	Ref	Expression
Assertion	wl-dfclab	⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑥 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 ∈ { 𝑦 ∣ 𝜑 } ) )
2		wl-clabv	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
3		sbequ	⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) )
4	2 3	bitrid	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑥 / 𝑦 ] 𝜑 ) )
5	4	pm5.32i	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑧 ∈ { 𝑦 ∣ 𝜑 } ) ↔ ( 𝑧 = 𝑥 ∧ [ 𝑥 / 𝑦 ] 𝜑 ) )
6	5	exbii	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 ∈ { 𝑦 ∣ 𝜑 } ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ [ 𝑥 / 𝑦 ] 𝜑 ) )
7		19.41v	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ [ 𝑥 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑧 𝑧 = 𝑥 ∧ [ 𝑥 / 𝑦 ] 𝜑 ) )
8		ax6ev	⊢ ∃ 𝑧 𝑧 = 𝑥
9	8	biantrur	⊢ ( [ 𝑥 / 𝑦 ] 𝜑 ↔ ( ∃ 𝑧 𝑧 = 𝑥 ∧ [ 𝑥 / 𝑦 ] 𝜑 ) )
10	7 9	bitr4i	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ [ 𝑥 / 𝑦 ] 𝜑 ) ↔ [ 𝑥 / 𝑦 ] 𝜑 )
11	1 6 10	3bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑥 / 𝑦 ] 𝜑 )