Description: Justification theorem for bj-df-v . See also vjust . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-vjust | ⊢ { 𝑥 ∣ ⊤ } = { 𝑦 ∣ ⊤ } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab | ⊢ ( 𝑧 ∈ { 𝑥 ∣ ⊤ } ↔ [ 𝑧 / 𝑥 ] ⊤ ) | |
2 | sbv | ⊢ ( [ 𝑧 / 𝑦 ] ⊤ ↔ ⊤ ) | |
3 | df-clab | ⊢ ( 𝑧 ∈ { 𝑦 ∣ ⊤ } ↔ [ 𝑧 / 𝑦 ] ⊤ ) | |
4 | sbv | ⊢ ( [ 𝑧 / 𝑥 ] ⊤ ↔ ⊤ ) | |
5 | 2 3 4 | 3bitr4ri | ⊢ ( [ 𝑧 / 𝑥 ] ⊤ ↔ 𝑧 ∈ { 𝑦 ∣ ⊤ } ) |
6 | 1 5 | bitri | ⊢ ( 𝑧 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑧 ∈ { 𝑦 ∣ ⊤ } ) |
7 | 6 | eqriv | ⊢ { 𝑥 ∣ ⊤ } = { 𝑦 ∣ ⊤ } |