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