This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ideq2

Description: For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020) (Revised by Peter Mazsa, 18-Dec-2021)

		Ref	Expression
	Assertion	ideq2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brid	⊢ ( 𝐴 I 𝐵 ↔ 𝐵 I 𝐴 )
2		ideqg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 I 𝐴 ↔ 𝐵 = 𝐴 ) )
3		eqcom	⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
4	2 3	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 I 𝐴 ↔ 𝐴 = 𝐵 ) )
5	1 4	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )