Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-idreseq Structured version   Visualization version   GIF version

Theorem bj-idreseq 34467
 Description: Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 34462 with V substituted for 𝑉 is a direct consequence of bj-idreseq 34467. This is a strengthening of resieq 5836 which should be proved from it (note that currently, resieq 5836 relies on ideq 5695). 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.
StepHypRef Expression
1 bj-brresdm 34451 . . . 4 (𝐴( I ↾ 𝐶)𝐵𝐴𝐶)
2 relres 5854 . . . . 5 Rel ( I ↾ 𝐶)
32brrelex2i 5581 . . . 4 (𝐴( I ↾ 𝐶)𝐵𝐵 ∈ V)
41, 3jca 514 . . 3 (𝐴( I ↾ 𝐶)𝐵 → (𝐴𝐶𝐵 ∈ V))
54adantl 484 . 2 (((𝐴𝐵) ∈ 𝐶𝐴( I ↾ 𝐶)𝐵) → (𝐴𝐶𝐵 ∈ V))
6 eqimss 3998 . . . . . 6 (𝐴 = 𝐵𝐴𝐵)
7 df-ss 3926 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
86, 7sylib 220 . . . . 5 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐴)
98adantl 484 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) = 𝐴)
10 simpl 485 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) ∈ 𝐶)
119, 10eqeltrrd 2912 . . 3 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐴𝐶)
12 eqimss2 3999 . . . . . . 7 (𝐴 = 𝐵𝐵𝐴)
13 sseqin2 4166 . . . . . . 7 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐵)
1412, 13sylib 220 . . . . . 6 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐵)
1514adantl 484 . . . . 5 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) = 𝐵)
1615, 10eqeltrrd 2912 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐵𝐶)
1716elexd 3490 . . 3 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐵 ∈ V)
1811, 17jca 514 . 2 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐶𝐵 ∈ V))
19 brres 5832 . . . 4 (𝐵 ∈ V → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴𝐶𝐴 I 𝐵)))
2019adantl 484 . . 3 ((𝐴𝐶𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴𝐶𝐴 I 𝐵)))
21 eqeq12 2834 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑥 = 𝑦𝐴 = 𝐵))
22 df-id 5432 . . . . 5 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
2321, 22brabga 5393 . . . 4 ((𝐴𝐶𝐵 ∈ V) → (𝐴 I 𝐵𝐴 = 𝐵))
2423anbi2d 630 . . 3 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 I 𝐵) ↔ (𝐴𝐶𝐴 = 𝐵)))
25 simp3 1134 . . . . 5 (((𝐴𝐶𝐵 ∈ V) ∧ 𝐴𝐶𝐴 = 𝐵) → 𝐴 = 𝐵)
26253expib 1118 . . . 4 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 = 𝐵) → 𝐴 = 𝐵))
27 3simpb 1145 . . . . 5 ((𝐴𝐶𝐵 ∈ V ∧ 𝐴 = 𝐵) → (𝐴𝐶𝐴 = 𝐵))
28273expia 1117 . . . 4 ((𝐴𝐶𝐵 ∈ V) → (𝐴 = 𝐵 → (𝐴𝐶𝐴 = 𝐵)))
2926, 28impbid 214 . . 3 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 = 𝐵) ↔ 𝐴 = 𝐵))
3020, 24, 293bitrd 307 . 2 ((𝐴𝐶𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵𝐴 = 𝐵))
315, 18, 30pm5.21nd 800 1 ((𝐴𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Vcvv 3470   ∩ cin 3908   ⊆ wss 3909   class class class wbr 5038   I cid 5431   ↾ cres 5529 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5175  ax-nul 5182  ax-pr 5302 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3472  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-br 5039  df-opab 5101  df-id 5432  df-xp 5533  df-rel 5534  df-res 5539 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator