Theorem ideqg

Description: For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	ideqg	$$⊢B\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢B\in V\to B\in V$$
2		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
3	2	brrelex1i	$$⊢A\mathrm{I}B\to A\in \mathrm{V}$$
4	1 3	anim12ci	$$⊢\left(B\in V\wedge A\mathrm{I}B\right)\to \left(A\in \mathrm{V}\wedge B\in V\right)$$
5		eleq1	$$⊢A=B\to \left(A\in V\leftrightarrow B\in V\right)$$
6	5	biimparc	$$⊢\left(B\in V\wedge A=B\right)\to A\in V$$
7	6	elexd	$$⊢\left(B\in V\wedge A=B\right)\to A\in \mathrm{V}$$
8		simpl	$$⊢\left(B\in V\wedge A=B\right)\to B\in V$$
9	7 8	jca	$$⊢\left(B\in V\wedge A=B\right)\to \left(A\in \mathrm{V}\wedge B\in V\right)$$
10		eqeq1	$$⊢x=A\to \left(x=y\leftrightarrow A=y\right)$$
11		eqeq2	$$⊢y=B\to \left(A=y\leftrightarrow A=B\right)$$
12		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
13	10 11 12	brabg	$$⊢\left(A\in \mathrm{V}\wedge B\in V\right)\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$
14	4 9 13	pm5.21nd	$$⊢B\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$