Theorem elid

Description: Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 after elrid . (Contributed by BJ, 28-Aug-2022)

	Ref	Expression
Assertion	elid	⊢ ( 𝐴 ∈ I ↔ ∃ 𝑥 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		reli	⊢ Rel I
2		dfrel3	⊢ ( Rel I ↔ ( I ↾ V ) = I )
3	1 2	mpbi	⊢ ( I ↾ V ) = I
4	3	eqcomi	⊢ I = ( I ↾ V )
5	4	eleq2i	⊢ ( 𝐴 ∈ I ↔ 𝐴 ∈ ( I ↾ V ) )
6		elrid	⊢ ( 𝐴 ∈ ( I ↾ V ) ↔ ∃ 𝑥 ∈ V 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ )
7		rexv	⊢ ( ∃ 𝑥 ∈ V 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ )
8	5 6 7	3bitri	⊢ ( 𝐴 ∈ I ↔ ∃ 𝑥 𝐴 = ⟨ 𝑥 , 𝑥 ⟩ )