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

Theorem reu2eqd 3370
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 3361 . . . . 5 (∃!𝑥𝐴 𝜓 ↔ (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
53, 4sylib 207 . . . 4 (𝜑 → (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
65simprd 478 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦))
7 reu2eqd.4 . . . 4 (𝜑𝐵𝐴)
8 reu2eqd.5 . . . 4 (𝜑𝐶𝐴)
9 nfv 1830 . . . . . . 7 𝑥𝜒
10 nfs1v 2425 . . . . . . 7 𝑥[𝑦 / 𝑥]𝜓
119, 10nfan 1816 . . . . . 6 𝑥(𝜒 ∧ [𝑦 / 𝑥]𝜓)
12 nfv 1830 . . . . . 6 𝑥 𝐵 = 𝑦
1311, 12nfim 1813 . . . . 5 𝑥((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)
14 nfv 1830 . . . . 5 𝑦((𝜒𝜃) → 𝐵 = 𝐶)
15 reu2eqd.1 . . . . . . 7 (𝑥 = 𝐵 → (𝜓𝜒))
1615anbi1d 737 . . . . . 6 (𝑥 = 𝐵 → ((𝜓 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒 ∧ [𝑦 / 𝑥]𝜓)))
17 eqeq1 2614 . . . . . 6 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
1816, 17imbi12d 333 . . . . 5 (𝑥 = 𝐵 → (((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) ↔ ((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)))
19 nfv 1830 . . . . . . . 8 𝑥𝜃
20 reu2eqd.2 . . . . . . . 8 (𝑥 = 𝐶 → (𝜓𝜃))
2119, 20sbhypf 3226 . . . . . . 7 (𝑦 = 𝐶 → ([𝑦 / 𝑥]𝜓𝜃))
2221anbi2d 736 . . . . . 6 (𝑦 = 𝐶 → ((𝜒 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒𝜃)))
23 eqeq2 2621 . . . . . 6 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
2422, 23imbi12d 333 . . . . 5 (𝑦 = 𝐶 → (((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦) ↔ ((𝜒𝜃) → 𝐵 = 𝐶)))
2513, 14, 18, 24rspc2 3292 . . . 4 ((𝐵𝐴𝐶𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
267, 8, 25syl2anc 691 . . 3 (𝜑 → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
276, 26mpd 15 . 2 (𝜑 → ((𝜒𝜃) → 𝐵 = 𝐶))
281, 2, 27mp2and 711 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  [wsb 1867  wcel 1977  wral 2896  wrex 2897  ∃!wreu 2898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-reu 2903  df-v 3175
This theorem is referenced by:  qtophmeo  21430  footeq  25416  mideulem2  25426  lmieq  25483
  Copyright terms: Public domain W3C validator