Description: Lemma for bj-denotes . (Contributed by BJ, 24-Apr-2024) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-denoteslem | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ { 𝑦 ∣ ⊤ } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vextru | ⊢ 𝑥 ∈ { 𝑦 ∣ ⊤ } | |
2 | 1 | biantru | ⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ { 𝑦 ∣ ⊤ } ) ) |
3 | 2 | exbii | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ { 𝑦 ∣ ⊤ } ) ) |
4 | dfclel | ⊢ ( 𝐴 ∈ { 𝑦 ∣ ⊤ } ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ { 𝑦 ∣ ⊤ } ) ) | |
5 | 3 4 | bitr4i | ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ { 𝑦 ∣ ⊤ } ) |