Theorem bj-idreseq 37157

Description: Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 37152 with V substituted for 𝑉 is a direct consequence of bj-idreseq 37157. This is a strengthening of resieq 5964 which should be proved from it (note that currently, resieq 5964 relies on ideq 5819). 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 37141	. . . 4 ⊢ (𝐴( I ↾ 𝐶)𝐵 → 𝐴 ∈ 𝐶)
2		relres 5979	. . . . 5 ⊢ Rel ( I ↾ 𝐶)
3	2	brrelex2i 5698	. . . 4 ⊢ (𝐴( I ↾ 𝐶)𝐵 → 𝐵 ∈ V)
4	1, 3	jca 511	. . 3 ⊢ (𝐴( I ↾ 𝐶)𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
5	4	adantl 481	. 2 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴( I ↾ 𝐶)𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
6		eqimss 4008	. . . . . 6 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
7		dfss2 3935	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
8	6, 7	sylib 218	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
9	8	adantl 481	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
10		simpl 482	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) ∈ 𝐶)
11	9, 10	eqeltrrd 2830	. . 3 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐶)
12		eqimss2 4009	. . . . . . 7 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
13		sseqin2 4189	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 𝐵)
14	12, 13	sylib 218	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐵)
15	14	adantl 481	. . . . 5 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) = 𝐵)
16	15, 10	eqeltrrd 2830	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝐶)
17	16	elexd 3474	. . 3 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐵 ∈ V)
18	11, 17	jca 511	. 2 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐶 ∧ 𝐴 = 𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V))
19		brres 5960	. . . 4 ⊢ (𝐵 ∈ V → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵)))
20	19	adantl 481	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵)))
21		eqeq12 2747	. . . . 5 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥 = 𝑦 ↔ 𝐴 = 𝐵))
22		df-id 5536	. . . . 5 ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
23	21, 22	brabga 5497	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
24	23	anbi2d 630	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐴 I 𝐵) ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵)))
25		simp3 1138	. . . . 5 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) ∧ 𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
26	25	3expib 1122	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵))
27		3simpb 1149	. . . . 5 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ∧ 𝐴 = 𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵))
28	27	3expia 1121	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵)))
29	26, 28	impbid 212	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵) ↔ 𝐴 = 𝐵))
30	20, 24, 29	3bitrd 305	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ 𝐴 = 𝐵))
31	5, 18, 30	pm5.21nd 801	1 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵 ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917   class class class wbr 5110   I cid 5535   ↾ cres 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-res 5653

This theorem is referenced by: (None)