Theorem elidinxpid

Description: Characterization of the elements of the intersection of the identity relation with a Cartesian square. (Contributed by Peter Mazsa, 9-Sep-2022)

	Ref	Expression
Assertion	elidinxpid	⊢ ( 𝐵 ∈ ( I ∩ ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = ⟨ 𝑥 , 𝑥 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		elidinxp	⊢ ( 𝐵 ∈ ( I ∩ ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) 𝐵 = ⟨ 𝑥 , 𝑥 ⟩ )
2		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
3	2	rexeqi	⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) 𝐵 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = ⟨ 𝑥 , 𝑥 ⟩ )
4	1 3	bitri	⊢ ( 𝐵 ∈ ( I ∩ ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = ⟨ 𝑥 , 𝑥 ⟩ )