Theorem bj-ideqg1

Description: For sets, the identity relation is the same thing as equality. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Generalize to a disjunctive antecedent. (Revised by BJ, 24-Dec-2023)

TODO: delete once bj-ideqg is in the main section.

	Ref	Expression
Assertion	bj-ideqg1	|- ( ( A e. V \/ B e. W ) -> ( A _I B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq12	|- ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) )
2		df-id	|- _I = { <. x , y >. | x = y }
3	1 2	bj-brab2a1	|- ( A _I B <-> ( ( A e. _V /\ B e. _V ) /\ A = B ) )
4		simpr	|- ( ( ( A e. _V /\ B e. _V ) /\ A = B ) -> A = B )
5		elex	|- ( A e. V -> A e. _V )
6	5	a1d	|- ( A e. V -> ( A = B -> A e. _V ) )
7		elex	|- ( B e. W -> B e. _V )
8		eleq1a	|- ( B e. _V -> ( A = B -> A e. _V ) )
9	7 8	syl	|- ( B e. W -> ( A = B -> A e. _V ) )
10	6 9	jaoi	|- ( ( A e. V \/ B e. W ) -> ( A = B -> A e. _V ) )
11		eleq1	|- ( A = B -> ( A e. _V <-> B e. _V ) )
12	5 11	syl5ibcom	|- ( A e. V -> ( A = B -> B e. _V ) )
13	7	a1d	|- ( B e. W -> ( A = B -> B e. _V ) )
14	12 13	jaoi	|- ( ( A e. V \/ B e. W ) -> ( A = B -> B e. _V ) )
15	10 14	jcad	|- ( ( A e. V \/ B e. W ) -> ( A = B -> ( A e. _V /\ B e. _V ) ) )
16	15	ancrd	|- ( ( A e. V \/ B e. W ) -> ( A = B -> ( ( A e. _V /\ B e. _V ) /\ A = B ) ) )
17	4 16	impbid2	|- ( ( A e. V \/ B e. W ) -> ( ( ( A e. _V /\ B e. _V ) /\ A = B ) <-> A = B ) )
18	3 17	syl5bb	|- ( ( A e. V \/ B e. W ) -> ( A _I B <-> A = B ) )