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 36346
Description: Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 36341 with V substituted for 𝑉 is a direct consequence of bj-idreseq 36346. This is a strengthening of resieq 5991 which should be proved from it (note that currently, resieq 5991 relies on ideq 5851). 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 36330 . . . 4 (𝐴( I ↾ 𝐶)𝐵𝐴𝐶)
2 relres 6009 . . . . 5 Rel ( I ↾ 𝐶)
32brrelex2i 5732 . . . 4 (𝐴( I ↾ 𝐶)𝐵𝐵 ∈ V)
41, 3jca 510 . . 3 (𝐴( I ↾ 𝐶)𝐵 → (𝐴𝐶𝐵 ∈ V))
54adantl 480 . 2 (((𝐴𝐵) ∈ 𝐶𝐴( I ↾ 𝐶)𝐵) → (𝐴𝐶𝐵 ∈ V))
6 eqimss 4039 . . . . . 6 (𝐴 = 𝐵𝐴𝐵)
7 df-ss 3964 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
86, 7sylib 217 . . . . 5 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐴)
98adantl 480 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) = 𝐴)
10 simpl 481 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) ∈ 𝐶)
119, 10eqeltrrd 2832 . . 3 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐴𝐶)
12 eqimss2 4040 . . . . . . 7 (𝐴 = 𝐵𝐵𝐴)
13 sseqin2 4214 . . . . . . 7 (𝐵𝐴 ↔ (𝐴𝐵) = 𝐵)
1412, 13sylib 217 . . . . . 6 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐵)
1514adantl 480 . . . . 5 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐵) = 𝐵)
1615, 10eqeltrrd 2832 . . . 4 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐵𝐶)
1716elexd 3493 . . 3 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → 𝐵 ∈ V)
1811, 17jca 510 . 2 (((𝐴𝐵) ∈ 𝐶𝐴 = 𝐵) → (𝐴𝐶𝐵 ∈ V))
19 brres 5987 . . . 4 (𝐵 ∈ V → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴𝐶𝐴 I 𝐵)))
2019adantl 480 . . 3 ((𝐴𝐶𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴𝐶𝐴 I 𝐵)))
21 eqeq12 2747 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑥 = 𝑦𝐴 = 𝐵))
22 df-id 5573 . . . . 5 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
2321, 22brabga 5533 . . . 4 ((𝐴𝐶𝐵 ∈ V) → (𝐴 I 𝐵𝐴 = 𝐵))
2423anbi2d 627 . . 3 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 I 𝐵) ↔ (𝐴𝐶𝐴 = 𝐵)))
25 simp3 1136 . . . . 5 (((𝐴𝐶𝐵 ∈ V) ∧ 𝐴𝐶𝐴 = 𝐵) → 𝐴 = 𝐵)
26253expib 1120 . . . 4 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 = 𝐵) → 𝐴 = 𝐵))
27 3simpb 1147 . . . . 5 ((𝐴𝐶𝐵 ∈ V ∧ 𝐴 = 𝐵) → (𝐴𝐶𝐴 = 𝐵))
28273expia 1119 . . . 4 ((𝐴𝐶𝐵 ∈ V) → (𝐴 = 𝐵 → (𝐴𝐶𝐴 = 𝐵)))
2926, 28impbid 211 . . 3 ((𝐴𝐶𝐵 ∈ V) → ((𝐴𝐶𝐴 = 𝐵) ↔ 𝐴 = 𝐵))
3020, 24, 293bitrd 304 . 2 ((𝐴𝐶𝐵 ∈ V) → (𝐴( I ↾ 𝐶)𝐵𝐴 = 𝐵))
315, 18, 30pm5.21nd 798 1 ((𝐴𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wcel 2104  Vcvv 3472  cin 3946  wss 3947   class class class wbr 5147   I cid 5572  cres 5677
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-res 5687
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator