Description: Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022) (Proof shortened by Peter Mazsa, 9-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | elrid | ⊢ ( 𝐴 ∈ ( I ↾ 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 𝐴 = 〈 𝑥 , 𝑥 〉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res | ⊢ ( I ↾ 𝑋 ) = ( I ∩ ( 𝑋 × V ) ) | |
2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ ( I ↾ 𝑋 ) ↔ 𝐴 ∈ ( I ∩ ( 𝑋 × V ) ) ) |
3 | elidinxp | ⊢ ( 𝐴 ∈ ( I ∩ ( 𝑋 × V ) ) ↔ ∃ 𝑥 ∈ ( 𝑋 ∩ V ) 𝐴 = 〈 𝑥 , 𝑥 〉 ) | |
4 | inv1 | ⊢ ( 𝑋 ∩ V ) = 𝑋 | |
5 | 4 | rexeqi | ⊢ ( ∃ 𝑥 ∈ ( 𝑋 ∩ V ) 𝐴 = 〈 𝑥 , 𝑥 〉 ↔ ∃ 𝑥 ∈ 𝑋 𝐴 = 〈 𝑥 , 𝑥 〉 ) |
6 | 2 3 5 | 3bitri | ⊢ ( 𝐴 ∈ ( I ↾ 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 𝐴 = 〈 𝑥 , 𝑥 〉 ) |