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\cap B\in C\to \left(A\left({\mathrm{I}\upharpoonright }_C\right)B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-brresdm	$$⊢A\left({\mathrm{I}\upharpoonright }_C\right)B\to A\in C$$
2		relres	$$⊢\mathrm{Rel}\left({\mathrm{I}\upharpoonright }_C\right)$$
3	2	brrelex2i	$$⊢A\left({\mathrm{I}\upharpoonright }_C\right)B\to B\in \mathrm{V}$$
4	1 3	jca	$$⊢A\left({\mathrm{I}\upharpoonright }_C\right)B\to \left(A\in C\wedge B\in \mathrm{V}\right)$$
5	4	adantl	$$⊢\left(A\cap B\in C\wedge A\left({\mathrm{I}\upharpoonright }_C\right)B\right)\to \left(A\in C\wedge B\in \mathrm{V}\right)$$
6		eqimss	$$⊢A=B\to A\subseteq B$$
7		df-ss	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
8	6 7	sylib	$$⊢A=B\to A\cap B=A$$
9	8	adantl	$$⊢\left(A\cap B\in C\wedge A=B\right)\to A\cap B=A$$
10		simpl	$$⊢\left(A\cap B\in C\wedge A=B\right)\to A\cap B\in C$$
11	9 10	eqeltrrd	$$⊢\left(A\cap B\in C\wedge A=B\right)\to A\in C$$
12		eqimss2	$$⊢A=B\to B\subseteq A$$
13		sseqin2	$$⊢B\subseteq A\leftrightarrow A\cap B=B$$
14	12 13	sylib	$$⊢A=B\to A\cap B=B$$
15	14	adantl	$$⊢\left(A\cap B\in C\wedge A=B\right)\to A\cap B=B$$
16	15 10	eqeltrrd	$$⊢\left(A\cap B\in C\wedge A=B\right)\to B\in C$$
17	16	elexd	$$⊢\left(A\cap B\in C\wedge A=B\right)\to B\in \mathrm{V}$$
18	11 17	jca	$$⊢\left(A\cap B\in C\wedge A=B\right)\to \left(A\in C\wedge B\in \mathrm{V}\right)$$
19		brres	$$⊢B\in \mathrm{V}\to \left(A\left({\mathrm{I}\upharpoonright }_C\right)B\leftrightarrow \left(A\in C\wedge A\mathrm{I}B\right)\right)$$
20	19	adantl	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(A\left({\mathrm{I}\upharpoonright }_C\right)B\leftrightarrow \left(A\in C\wedge A\mathrm{I}B\right)\right)$$
21		eqeq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x=y\leftrightarrow A=B\right)$$
22		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
23	21 22	brabga	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$
24	23	anbi2d	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(\left(A\in C\wedge A\mathrm{I}B\right)\leftrightarrow \left(A\in C\wedge A=B\right)\right)$$
25		simp3	$$⊢\left(\left(A\in C\wedge B\in \mathrm{V}\right)\wedge A\in C\wedge A=B\right)\to A=B$$
26	25	3expib	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(\left(A\in C\wedge A=B\right)\to A=B\right)$$
27		3simpb	$$⊢\left(A\in C\wedge B\in \mathrm{V}\wedge A=B\right)\to \left(A\in C\wedge A=B\right)$$
28	27	3expia	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(A=B\to \left(A\in C\wedge A=B\right)\right)$$
29	26 28	impbid	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(\left(A\in C\wedge A=B\right)\leftrightarrow A=B\right)$$
30	20 24 29	3bitrd	$$⊢\left(A\in C\wedge B\in \mathrm{V}\right)\to \left(A\left({\mathrm{I}\upharpoonright }_C\right)B\leftrightarrow A=B\right)$$
31	5 18 30	pm5.21nd	$$⊢A\cap B\in C\to \left(A\left({\mathrm{I}\upharpoonright }_C\right)B\leftrightarrow A=B\right)$$