Metamath Proof Explorer


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 bj-denotes ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 )
8 7 a1i ( ∀ 𝑥 𝜑 → ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) )
9 2 6 8 3bitrd ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ { 𝑥𝜑 } ↔ ∃ 𝑦 𝑦 = 𝐴 ) )