Description: The converse of the identity relation. Theorem 3.7(ii) of Monk1 p. 36. (Contributed by NM, 26-Apr-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvi | ⊢ ◡ I = I |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | ⊢ 𝑥 ∈ V | |
| 2 | 1 | ideq | ⊢ ( 𝑦 I 𝑥 ↔ 𝑦 = 𝑥 ) |
| 3 | equcom | ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 ) | |
| 4 | 2 3 | bitri | ⊢ ( 𝑦 I 𝑥 ↔ 𝑥 = 𝑦 ) |
| 5 | 4 | opabbii | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 I 𝑥 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } |
| 6 | df-cnv | ⊢ ◡ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 I 𝑥 } | |
| 7 | df-id | ⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } | |
| 8 | 5 6 7 | 3eqtr4i | ⊢ ◡ I = I |