Metamath Proof Explorer


Theorem elrid

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 ↾ 𝑋 ) ↔ ∃ 𝑥𝑋 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ )

Proof

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 ↾ 𝑋 ) ↔ ∃ 𝑥𝑋 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ )