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 |