Theorem bj-idreseq

Description: Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg with _V substituted for V is a direct consequence of bj-idreseq . This is a strengthening of resieq which should be proved from it (note that currently, resieq relies on ideq ). Note that the intersection in the antecedent is not very meaningful, but is a device to prove versions with either class assumed to be a set. It could be enough to prove the version with a disjunctive antecedent: |- ( ( A e. C \/ B e. C ) -> ... ) . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Assertion	bj-idreseq	|- ( ( A i^i B ) e. C -> ( A ( _I |` C ) B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		bj-brresdm	|- ( A ( _I |` C ) B -> A e. C )
2		relres	|- Rel ( _I |` C )
3	2	brrelex2i	|- ( A ( _I |` C ) B -> B e. _V )
4	1 3	jca	|- ( A ( _I |` C ) B -> ( A e. C /\ B e. _V ) )
5	4	adantl	|- ( ( ( A i^i B ) e. C /\ A ( _I |` C ) B ) -> ( A e. C /\ B e. _V ) )
6		eqimss	|- ( A = B -> A C_ B )
7		df-ss	|- ( A C_ B <-> ( A i^i B ) = A )
8	6 7	sylib	|- ( A = B -> ( A i^i B ) = A )
9	8	adantl	|- ( ( ( A i^i B ) e. C /\ A = B ) -> ( A i^i B ) = A )
10		simpl	|- ( ( ( A i^i B ) e. C /\ A = B ) -> ( A i^i B ) e. C )
11	9 10	eqeltrrd	|- ( ( ( A i^i B ) e. C /\ A = B ) -> A e. C )
12		eqimss2	|- ( A = B -> B C_ A )
13		sseqin2	|- ( B C_ A <-> ( A i^i B ) = B )
14	12 13	sylib	|- ( A = B -> ( A i^i B ) = B )
15	14	adantl	|- ( ( ( A i^i B ) e. C /\ A = B ) -> ( A i^i B ) = B )
16	15 10	eqeltrrd	|- ( ( ( A i^i B ) e. C /\ A = B ) -> B e. C )
17	16	elexd	|- ( ( ( A i^i B ) e. C /\ A = B ) -> B e. _V )
18	11 17	jca	|- ( ( ( A i^i B ) e. C /\ A = B ) -> ( A e. C /\ B e. _V ) )
19		brres	|- ( B e. _V -> ( A ( _I |` C ) B <-> ( A e. C /\ A _I B ) ) )
20	19	adantl	|- ( ( A e. C /\ B e. _V ) -> ( A ( _I |` C ) B <-> ( A e. C /\ A _I B ) ) )
21		eqeq12	|- ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) )
22		df-id	|- _I = { <. x , y >. | x = y }
23	21 22	brabga	|- ( ( A e. C /\ B e. _V ) -> ( A _I B <-> A = B ) )
24	23	anbi2d	|- ( ( A e. C /\ B e. _V ) -> ( ( A e. C /\ A _I B ) <-> ( A e. C /\ A = B ) ) )
25		simp3	|- ( ( ( A e. C /\ B e. _V ) /\ A e. C /\ A = B ) -> A = B )
26	25	3expib	|- ( ( A e. C /\ B e. _V ) -> ( ( A e. C /\ A = B ) -> A = B ) )
27		3simpb	|- ( ( A e. C /\ B e. _V /\ A = B ) -> ( A e. C /\ A = B ) )
28	27	3expia	|- ( ( A e. C /\ B e. _V ) -> ( A = B -> ( A e. C /\ A = B ) ) )
29	26 28	impbid	|- ( ( A e. C /\ B e. _V ) -> ( ( A e. C /\ A = B ) <-> A = B ) )
30	20 24 29	3bitrd	|- ( ( A e. C /\ B e. _V ) -> ( A ( _I |` C ) B <-> A = B ) )
31	5 18 30	pm5.21nd	|- ( ( A i^i B ) e. C -> ( A ( _I |` C ) B <-> A = B ) )