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	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 → ( 𝐴 ( I ↾ 𝐶 ) 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-brresdm	⊢ ( 𝐴 ( I ↾ 𝐶 ) 𝐵 → 𝐴 ∈ 𝐶 )
2		relres	⊢ Rel ( I ↾ 𝐶 )
3	2	brrelex2i	⊢ ( 𝐴 ( I ↾ 𝐶 ) 𝐵 → 𝐵 ∈ V )
4	1 3	jca	⊢ ( 𝐴 ( I ↾ 𝐶 ) 𝐵 → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) )
5	4	adantl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 ( I ↾ 𝐶 ) 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) )
6		eqimss	⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
7		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
8	6 7	sylib	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
9	8	adantl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
10		simpl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 )
11	9 10	eqeltrrd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝐶 )
12		eqimss2	⊢ ( 𝐴 = 𝐵 → 𝐵 ⊆ 𝐴 )
13		sseqin2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
14	12 13	sylib	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
15	14	adantl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
16	15 10	eqeltrrd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝐶 )
17	16	elexd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
18	11 17	jca	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) )
19		brres	⊢ ( 𝐵 ∈ V → ( 𝐴 ( I ↾ 𝐶 ) 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵 ) ) )
20	19	adantl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( 𝐴 ( I ↾ 𝐶 ) 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵 ) ) )
21		eqeq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) )
22		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
23	21 22	brabga	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )
24	23	anbi2d	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵 ) ) )
25		simp3	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
26	25	3expib	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 ) )
27		3simpb	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵 ) )
28	27	3expia	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵 ) ) )
29	26 28	impbid	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵 ) ↔ 𝐴 = 𝐵 ) )
30	20 24 29	3bitrd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ) → ( 𝐴 ( I ↾ 𝐶 ) 𝐵 ↔ 𝐴 = 𝐵 ) )
31	5 18 30	pm5.21nd	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 → ( 𝐴 ( I ↾ 𝐶 ) 𝐵 ↔ 𝐴 = 𝐵 ) )