MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reu2eqd Structured version   Visualization version   GIF version

Theorem reu2eqd 3678
Description: Deduce equality from restricted uniqueness, deduction version. (Contributed by Thierry Arnoux, 27-Nov-2019.)
Hypotheses
Ref Expression
reu2eqd.1 (𝑥 = 𝐵 → (𝜓𝜒))
reu2eqd.2 (𝑥 = 𝐶 → (𝜓𝜃))
reu2eqd.3 (𝜑 → ∃!𝑥𝐴 𝜓)
reu2eqd.4 (𝜑𝐵𝐴)
reu2eqd.5 (𝜑𝐶𝐴)
reu2eqd.6 (𝜑𝜒)
reu2eqd.7 (𝜑𝜃)
Assertion
Ref Expression
reu2eqd (𝜑𝐵 = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝜒,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem reu2eqd
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 reu2eqd.6 . 2 (𝜑𝜒)
2 reu2eqd.7 . 2 (𝜑𝜃)
3 reu2eqd.3 . . . . 5 (𝜑 → ∃!𝑥𝐴 𝜓)
4 reu2 3667 . . . . 5 (∃!𝑥𝐴 𝜓 ↔ (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
53, 4sylib 221 . . . 4 (𝜑 → (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
65simprd 499 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦))
7 reu2eqd.4 . . . 4 (𝜑𝐵𝐴)
8 reu2eqd.5 . . . 4 (𝜑𝐶𝐴)
9 nfv 1915 . . . . . . 7 𝑥𝜒
10 nfs1v 2158 . . . . . . 7 𝑥[𝑦 / 𝑥]𝜓
119, 10nfan 1900 . . . . . 6 𝑥(𝜒 ∧ [𝑦 / 𝑥]𝜓)
12 nfv 1915 . . . . . 6 𝑥 𝐵 = 𝑦
1311, 12nfim 1897 . . . . 5 𝑥((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)
14 nfv 1915 . . . . 5 𝑦((𝜒𝜃) → 𝐵 = 𝐶)
15 reu2eqd.1 . . . . . . 7 (𝑥 = 𝐵 → (𝜓𝜒))
1615anbi1d 632 . . . . . 6 (𝑥 = 𝐵 → ((𝜓 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒 ∧ [𝑦 / 𝑥]𝜓)))
17 eqeq1 2805 . . . . . 6 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
1816, 17imbi12d 348 . . . . 5 (𝑥 = 𝐵 → (((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) ↔ ((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)))
19 nfv 1915 . . . . . . . 8 𝑥𝜃
20 reu2eqd.2 . . . . . . . 8 (𝑥 = 𝐶 → (𝜓𝜃))
2119, 20sbhypf 3503 . . . . . . 7 (𝑦 = 𝐶 → ([𝑦 / 𝑥]𝜓𝜃))
2221anbi2d 631 . . . . . 6 (𝑦 = 𝐶 → ((𝜒 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒𝜃)))
23 eqeq2 2813 . . . . . 6 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
2422, 23imbi12d 348 . . . . 5 (𝑦 = 𝐶 → (((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦) ↔ ((𝜒𝜃) → 𝐵 = 𝐶)))
2513, 14, 18, 24rspc2 3582 . . . 4 ((𝐵𝐴𝐶𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
267, 8, 25syl2anc 587 . . 3 (𝜑 → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
276, 26mpd 15 . 2 (𝜑 → ((𝜒𝜃) → 𝐵 = 𝐶))
281, 2, 27mp2and 698 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  [wsb 2069  wcel 2112  wral 3109  wrex 3110  ∃!wreu 3111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-reu 3116  df-v 3446
This theorem is referenced by:  qtophmeo  22426  footeq  26522  mideulem2  26532  lmieq  26589
  Copyright terms: Public domain W3C validator