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 e. V -> ( A _I B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( B e. V -> B e. V )
2		reli	|- Rel _I
3	2	brrelex1i	|- ( A _I B -> A e. _V )
4	1 3	anim12ci	|- ( ( B e. V /\ A _I B ) -> ( A e. _V /\ B e. V ) )
5		eleq1	|- ( A = B -> ( A e. V <-> B e. V ) )
6	5	biimparc	|- ( ( B e. V /\ A = B ) -> A e. V )
7	6	elexd	|- ( ( B e. V /\ A = B ) -> A e. _V )
8		simpl	|- ( ( B e. V /\ A = B ) -> B e. V )
9	7 8	jca	|- ( ( B e. V /\ A = B ) -> ( A e. _V /\ B e. V ) )
10		eqeq1	|- ( x = A -> ( x = y <-> A = y ) )
11		eqeq2	|- ( y = B -> ( A = y <-> A = B ) )
12		df-id	|- _I = { <. x , y >. | x = y }
13	10 11 12	brabg	|- ( ( A e. _V /\ B e. V ) -> ( A _I B <-> A = B ) )
14	4 9 13	pm5.21nd	|- ( B e. V -> ( A _I B <-> A = B ) )