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

Theorem reu2eqd 3436
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 3427 . . . . 5 (∃!𝑥𝐴 𝜓 ↔ (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
53, 4sylib 208 . . . 4 (𝜑 → (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
65simprd 478 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦))
7 reu2eqd.4 . . . 4 (𝜑𝐵𝐴)
8 reu2eqd.5 . . . 4 (𝜑𝐶𝐴)
9 nfv 1883 . . . . . . 7 𝑥𝜒
10 nfs1v 2465 . . . . . . 7 𝑥[𝑦 / 𝑥]𝜓
119, 10nfan 1868 . . . . . 6 𝑥(𝜒 ∧ [𝑦 / 𝑥]𝜓)
12 nfv 1883 . . . . . 6 𝑥 𝐵 = 𝑦
1311, 12nfim 1865 . . . . 5 𝑥((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)
14 nfv 1883 . . . . 5 𝑦((𝜒𝜃) → 𝐵 = 𝐶)
15 reu2eqd.1 . . . . . . 7 (𝑥 = 𝐵 → (𝜓𝜒))
1615anbi1d 741 . . . . . 6 (𝑥 = 𝐵 → ((𝜓 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒 ∧ [𝑦 / 𝑥]𝜓)))
17 eqeq1 2655 . . . . . 6 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
1816, 17imbi12d 333 . . . . 5 (𝑥 = 𝐵 → (((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) ↔ ((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)))
19 nfv 1883 . . . . . . . 8 𝑥𝜃
20 reu2eqd.2 . . . . . . . 8 (𝑥 = 𝐶 → (𝜓𝜃))
2119, 20sbhypf 3284 . . . . . . 7 (𝑦 = 𝐶 → ([𝑦 / 𝑥]𝜓𝜃))
2221anbi2d 740 . . . . . 6 (𝑦 = 𝐶 → ((𝜒 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒𝜃)))
23 eqeq2 2662 . . . . . 6 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
2422, 23imbi12d 333 . . . . 5 (𝑦 = 𝐶 → (((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦) ↔ ((𝜒𝜃) → 𝐵 = 𝐶)))
2513, 14, 18, 24rspc2 3351 . . . 4 ((𝐵𝐴𝐶𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
267, 8, 25syl2anc 694 . . 3 (𝜑 → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
276, 26mpd 15 . 2 (𝜑 → ((𝜒𝜃) → 𝐵 = 𝐶))
281, 2, 27mp2and 715 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  [wsb 1937  wcel 2030  wral 2941  wrex 2942  ∃!wreu 2943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-reu 2948  df-v 3233
This theorem is referenced by:  qtophmeo  21668  footeq  25661  mideulem2  25671  lmieq  25728
  Copyright terms: Public domain W3C validator