Theorem bj-idreseq 37655

Description: Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 37650 with V substituted for 𝑉 is a direct consequence of bj-idreseq 37655. This is a strengthening of resieq 5977 which should be proved from it (note that currently, resieq 5977 relies on ideq 5825). 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: ⊢ ((𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶) → ...). (Contributed by BJ, 25-Dec-2023.)

Assertion

Ref	Expression
bj-idreseq	⊢ ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵 ↔ 𝐴 = 𝐵))

Proof of Theorem bj-idreseq

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bj-brresdm 37639	. . . 4 ⊢ (𝐴( I ↾ 𝐶)𝐵 → 𝐴 ∈ 𝐶)
2		relres 5992	. . . . 5 ⊢ Rel ( I ↾ 𝐶)
3	2	brrelex2i 5705	. . . 4 ⊢ (𝐴( I ↾ 𝐶)𝐵 → 𝐵 ∈ V)
4	1, 3	jca 519	. . 3 ⊢ (𝐴( I ↾ 𝐶)𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
5	4	adantl 485	. 2 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴( I ↾ 𝐶)𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
6		eqimss 3995	. . . . . 6 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
7		dfss2 3923	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
8	6, 7	sylib 220	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
9	8	adantl 485	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
10		simpl 486	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) ∈ 𝐶)
11	9, 10	eqeltrrd 2864	. . 3 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐶)
12		eqimss2 3996	. . . . . . 7 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
13		sseqin2 4176	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 𝐵)
14	12, 13	sylib 220	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐵)
15	14	adantl 485	. . . . 5 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) = 𝐵)
16	15, 10	eqeltrrd 2864	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝐶)
17	16	elexd 3478	. . 3 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐵 ∈ V)
18	11, 17	jca 519	. 2 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
19		brres 5973	. . . 4 ⊢ (𝐵 ∈ V → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵)))
20	19	adantl 485	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵)))
21		eqeq12 2780	. . . . 5 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥 = 𝑦 ↔ 𝐴 = 𝐵))
22		df-id 5543	. . . . 5 ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
23	21, 22	brabga 5505	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
24	23	anbi2d 639	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵) ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵)))
25		simp3 1152	. . . . 5 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
26	25	3expib 1136	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵))
27		3simpb 1163	. . . . 5 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ∧ 𝐴 = 𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵))
28	27	3expia 1135	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵)))
29	26, 28	impbid 214	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵) ↔ 𝐴 = 𝐵))
30	20, 24, 29	3bitrd 307	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ 𝐴 = 𝐵))
31	5, 18, 30	pm5.21nd 811	1 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵 ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561   ∈ wcel 2143  Vcvv 3455   ∩ cin 3904   ⊆ wss 3905   class class class wbr 5101   I cid 5542   ↾ cres 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102  df-opab 5164  df-id 5543  df-xp 5654  df-rel 5655  df-res 5660

This theorem is referenced by: (None)