Theorem bj-issetwt

Description: Closed form of bj-issetw . (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-issetwt	⊢ ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 𝑦 = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) )
2	1	a1i	⊢ ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) )
3		vexwt	⊢ ( ∀ 𝑥 𝜑 → 𝑧 ∈ { 𝑥 ∣ 𝜑 } )
4	3	biantrud	⊢ ( ∀ 𝑥 𝜑 → ( 𝑧 = 𝐴 ↔ ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) )
5	4	bicomd	⊢ ( ∀ 𝑥 𝜑 → ( ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ 𝑧 = 𝐴 ) )
6	5	exbidv	⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑧 𝑧 = 𝐴 ) )
7		iseqsetv-clel	⊢ ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 )
8	7	a1i	⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) )
9	2 6 8	3bitrd	⊢ ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 𝑦 = 𝐴 ) )