Metamath Proof Explorer


Theorem bj-denoteslem

Description: Lemma for bj-denotes . (Contributed by BJ, 24-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Assertion bj-denoteslem ( ∃ 𝑥 𝑥 = 𝐴𝐴 ∈ { 𝑦 ∣ ⊤ } )

Proof

Step Hyp Ref Expression
1 vextru 𝑥 ∈ { 𝑦 ∣ ⊤ }
2 1 biantru ( 𝑥 = 𝐴 ↔ ( 𝑥 = 𝐴𝑥 ∈ { 𝑦 ∣ ⊤ } ) )
3 2 exbii ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐴𝑥 ∈ { 𝑦 ∣ ⊤ } ) )
4 dfclel ( 𝐴 ∈ { 𝑦 ∣ ⊤ } ↔ ∃ 𝑥 ( 𝑥 = 𝐴𝑥 ∈ { 𝑦 ∣ ⊤ } ) )
5 3 4 bitr4i ( ∃ 𝑥 𝑥 = 𝐴𝐴 ∈ { 𝑦 ∣ ⊤ } )