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

Theorem reu2eqd 3389
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 3380 . . . . 5 (∃!𝑥𝐴 𝜓 ↔ (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
53, 4sylib 208 . . . 4 (𝜑 → (∃𝑥𝐴 𝜓 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦)))
65simprd 479 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦))
7 reu2eqd.4 . . . 4 (𝜑𝐵𝐴)
8 reu2eqd.5 . . . 4 (𝜑𝐶𝐴)
9 nfv 1840 . . . . . . 7 𝑥𝜒
10 nfs1v 2436 . . . . . . 7 𝑥[𝑦 / 𝑥]𝜓
119, 10nfan 1825 . . . . . 6 𝑥(𝜒 ∧ [𝑦 / 𝑥]𝜓)
12 nfv 1840 . . . . . 6 𝑥 𝐵 = 𝑦
1311, 12nfim 1822 . . . . 5 𝑥((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)
14 nfv 1840 . . . . 5 𝑦((𝜒𝜃) → 𝐵 = 𝐶)
15 reu2eqd.1 . . . . . . 7 (𝑥 = 𝐵 → (𝜓𝜒))
1615anbi1d 740 . . . . . 6 (𝑥 = 𝐵 → ((𝜓 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒 ∧ [𝑦 / 𝑥]𝜓)))
17 eqeq1 2625 . . . . . 6 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
1816, 17imbi12d 334 . . . . 5 (𝑥 = 𝐵 → (((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) ↔ ((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦)))
19 nfv 1840 . . . . . . . 8 𝑥𝜃
20 reu2eqd.2 . . . . . . . 8 (𝑥 = 𝐶 → (𝜓𝜃))
2119, 20sbhypf 3242 . . . . . . 7 (𝑦 = 𝐶 → ([𝑦 / 𝑥]𝜓𝜃))
2221anbi2d 739 . . . . . 6 (𝑦 = 𝐶 → ((𝜒 ∧ [𝑦 / 𝑥]𝜓) ↔ (𝜒𝜃)))
23 eqeq2 2632 . . . . . 6 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
2422, 23imbi12d 334 . . . . 5 (𝑦 = 𝐶 → (((𝜒 ∧ [𝑦 / 𝑥]𝜓) → 𝐵 = 𝑦) ↔ ((𝜒𝜃) → 𝐵 = 𝐶)))
2513, 14, 18, 24rspc2 3308 . . . 4 ((𝐵𝐴𝐶𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
267, 8, 25syl2anc 692 . . 3 (𝜑 → (∀𝑥𝐴𝑦𝐴 ((𝜓 ∧ [𝑦 / 𝑥]𝜓) → 𝑥 = 𝑦) → ((𝜒𝜃) → 𝐵 = 𝐶)))
276, 26mpd 15 . 2 (𝜑 → ((𝜒𝜃) → 𝐵 = 𝐶))
281, 2, 27mp2and 714 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  [wsb 1877  wcel 1987  wral 2907  wrex 2908  ∃!wreu 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-reu 2914  df-v 3191
This theorem is referenced by:  qtophmeo  21543  footeq  25533  mideulem2  25543  lmieq  25600
  Copyright terms: Public domain W3C validator