Users' Mathboxes 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 37163
Description: Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 37158 with V substituted for 𝑉 is a direct consequence of bj-idreseq 37163. This is a strengthening of resieq 6008 which should be proved from it (note that currently, resieq 6008 relies on ideq 5863). 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 37147 . . . 4 (𝐴( I ↾ 𝐶)𝐵𝐴𝐶)
2 relres 6023 . . . . 5 Rel ( I ↾ 𝐶)
32brrelex2i 5742 . . . 4 (𝐴( I ↾ 𝐶)𝐵𝐵 ∈ V)
41, 3jca 511 . . 3 (𝐴( I ↾ 𝐶)𝐵 → (𝐴𝐶𝐵 ∈ V))
54adantl 481 . 2 (((𝐴𝐵) ∈ 𝐶𝐴( I ↾ 𝐶)𝐵) → (𝐴𝐶𝐵 ∈ V))
6 eqimss 4042 . . . . . 6 (𝐴 = 𝐵𝐴𝐵)
7 dfss2 3969 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
86, 7sylib 218 . . . . 5 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐴)
98adantl 481 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) = 𝐴)
10 simpl 482 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) ∈ 𝐶)
119, 10eqeltrrd 2842 . . 3 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐴𝐶)
12 eqimss2 4043 . . . . . . 7 (𝐴 = 𝐵𝐵𝐴)
13 sseqin2 4223 . . . . . . 7 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐵)
1412, 13sylib 218 . . . . . 6 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐵)
1514adantl 481 . . . . 5 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) = 𝐵)
1615, 10eqeltrrd 2842 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐵𝐶)
1716elexd 3504 . . 3 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐵 ∈ V)
1811, 17jca 511 . 2 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐶𝐵 ∈ V))
19 brres 6004 . . . 4 (𝐵 ∈ V → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴𝐶𝐴 I 𝐵)))
2019adantl 481 . . 3 ((𝐴𝐶𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴𝐶𝐴 I 𝐵)))
21 eqeq12 2754 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑥 = 𝑦𝐴 = 𝐵))
22 df-id 5578 . . . . 5 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
2321, 22brabga 5539 . . . 4 ((𝐴𝐶𝐵 ∈ V) → (𝐴 I 𝐵𝐴 = 𝐵))
2423anbi2d 630 . . 3 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 I 𝐵) ↔ (𝐴𝐶𝐴 = 𝐵)))
25 simp3 1139 . . . . 5 (((𝐴𝐶𝐵 ∈ V) ∧ 𝐴𝐶𝐴 = 𝐵) → 𝐴 = 𝐵)
26253expib 1123 . . . 4 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 = 𝐵) → 𝐴 = 𝐵))
27 3simpb 1150 . . . . 5 ((𝐴𝐶𝐵 ∈ V ∧ 𝐴 = 𝐵) → (𝐴𝐶𝐴 = 𝐵))
28273expia 1122 . . . 4 ((𝐴𝐶𝐵 ∈ V) → (𝐴 = 𝐵 → (𝐴𝐶𝐴 = 𝐵)))
2926, 28impbid 212 . . 3 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 = 𝐵) ↔ 𝐴 = 𝐵))
3020, 24, 293bitrd 305 . 2 ((𝐴𝐶𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵𝐴 = 𝐵))
315, 18, 30pm5.21nd 802 1 ((𝐴𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  Vcvv 3480  cin 3950  wss 3951   class class class wbr 5143   I cid 5577  cres 5687
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-res 5697
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator