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

Theorem reu2eqd 3745
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 3734 . . . . 5 (∃!𝑥𝐴 𝜓 ↔ (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
53, 4sylib 218 . . . 4 (𝜑 → (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
65simprd 495 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦))
7 reu2eqd.4 . . . 4 (𝜑𝐵𝐴)
8 reu2eqd.5 . . . 4 (𝜑𝐶𝐴)
9 nfv 1912 . . . . . . 7 𝑥𝜒
10 nfs1v 2154 . . . . . . 7 𝑥[𝑦 / 𝑥]𝜓
119, 10nfan 1897 . . . . . 6 𝑥(𝜒 ∧ [𝑦 / 𝑥]𝜓)
12 nfv 1912 . . . . . 6 𝑥 𝐵 = 𝑦
1311, 12nfim 1894 . . . . 5 𝑥((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)
14 nfv 1912 . . . . 5 𝑦((𝜒𝜃) → 𝐵 = 𝐶)
15 reu2eqd.1 . . . . . . 7 (𝑥 = 𝐵 → (𝜓𝜒))
1615anbi1d 631 . . . . . 6 (𝑥 = 𝐵 → ((𝜓 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒 ∧ [𝑦 / 𝑥]𝜓)))
17 eqeq1 2739 . . . . . 6 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
1816, 17imbi12d 344 . . . . 5 (𝑥 = 𝐵 → (((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) ↔ ((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)))
19 nfv 1912 . . . . . . . 8 𝑥𝜃
20 reu2eqd.2 . . . . . . . 8 (𝑥 = 𝐶 → (𝜓𝜃))
2119, 20sbhypf 3544 . . . . . . 7 (𝑦 = 𝐶 → ([𝑦 / 𝑥]𝜓𝜃))
2221anbi2d 630 . . . . . 6 (𝑦 = 𝐶 → ((𝜒 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒𝜃)))
23 eqeq2 2747 . . . . . 6 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
2422, 23imbi12d 344 . . . . 5 (𝑦 = 𝐶 → (((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦) ↔ ((𝜒𝜃) → 𝐵 = 𝐶)))
2513, 14, 18, 24rspc2 3631 . . . 4 ((𝐵𝐴𝐶𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
267, 8, 25syl2anc 584 . . 3 (𝜑 → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
276, 26mpd 15 . 2 (𝜑 → ((𝜒𝜃) → 𝐵 = 𝐶))
281, 2, 27mp2and 699 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  [wsb 2062  wcel 2106  wral 3059  wrex 3068  ∃!wreu 3376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-reu 3379
This theorem is referenced by:  qtophmeo  23841  footeq  28747  mideulem2  28757  lmieq  28814  upciclem3  48814
  Copyright terms: Public domain W3C validator