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

Theorem reu6 3536
Description: A way to express restricted uniqueness. (Contributed by NM, 20-Oct-2006.)
Assertion
Ref Expression
reu6 (∃!𝑥𝐴 𝜑 ↔ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reu6
StepHypRef Expression
1 df-reu 3057 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 19.28v 2074 . . . . 5 (∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ↔ (𝑦𝐴 ∧ ∀𝑥(𝑥𝐴 → (𝜑𝑥 = 𝑦))))
3 eleq1w 2822 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
4 sbequ12 2258 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
53, 4anbi12d 749 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)))
6 equequ1 2107 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 = 𝑦𝑦 = 𝑦))
75, 6bibi12d 334 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦)))
8 equid 2094 . . . . . . . . . . . 12 𝑦 = 𝑦
98tbt 358 . . . . . . . . . . 11 ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦))
10 simpl 474 . . . . . . . . . . 11 ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦𝐴)
119, 10sylbir 225 . . . . . . . . . 10 (((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦) → 𝑦𝐴)
127, 11syl6bi 243 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → 𝑦𝐴))
1312spimv 2402 . . . . . . . 8 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → 𝑦𝐴)
14 ibar 526 . . . . . . . . . . 11 (𝑥𝐴 → (𝜑 ↔ (𝑥𝐴𝜑)))
1514bibi1d 332 . . . . . . . . . 10 (𝑥𝐴 → ((𝜑𝑥 = 𝑦) ↔ ((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦)))
1615biimprcd 240 . . . . . . . . 9 (((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → (𝑥𝐴 → (𝜑𝑥 = 𝑦)))
1716sps 2202 . . . . . . . 8 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → (𝑥𝐴 → (𝜑𝑥 = 𝑦)))
1813, 17jca 555 . . . . . . 7 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → (𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))))
1918axc4i 2278 . . . . . 6 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → ∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))))
20 biimp 205 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
2120imim2i 16 . . . . . . . . . 10 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → (𝑥𝐴 → (𝜑𝑥 = 𝑦)))
2221impd 446 . . . . . . . . 9 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → ((𝑥𝐴𝜑) → 𝑥 = 𝑦))
2322adantl 473 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → ((𝑥𝐴𝜑) → 𝑥 = 𝑦))
24 eleq1a 2834 . . . . . . . . . . . 12 (𝑦𝐴 → (𝑥 = 𝑦𝑥𝐴))
2524adantr 472 . . . . . . . . . . 11 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → (𝑥 = 𝑦𝑥𝐴))
2625imp 444 . . . . . . . . . 10 (((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝑥𝐴)
27 biimpr 210 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
2827imim2i 16 . . . . . . . . . . . . 13 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → (𝑥𝐴 → (𝑥 = 𝑦𝜑)))
2928com23 86 . . . . . . . . . . . 12 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → (𝑥 = 𝑦 → (𝑥𝐴𝜑)))
3029imp 444 . . . . . . . . . . 11 (((𝑥𝐴 → (𝜑𝑥 = 𝑦)) ∧ 𝑥 = 𝑦) → (𝑥𝐴𝜑))
3130adantll 752 . . . . . . . . . 10 (((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝑥𝐴𝜑))
3226, 31jcai 560 . . . . . . . . 9 (((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝑥𝐴𝜑))
3332ex 449 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → (𝑥 = 𝑦 → (𝑥𝐴𝜑)))
3423, 33impbid 202 . . . . . . 7 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → ((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦))
3534alimi 1888 . . . . . 6 (∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → ∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦))
3619, 35impbii 199 . . . . 5 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))))
37 df-ral 3055 . . . . . 6 (∀𝑥𝐴 (𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝑥 = 𝑦)))
3837anbi2i 732 . . . . 5 ((𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)) ↔ (𝑦𝐴 ∧ ∀𝑥(𝑥𝐴 → (𝜑𝑥 = 𝑦))))
392, 36, 383bitr4i 292 . . . 4 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ (𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)))
4039exbii 1923 . . 3 (∃𝑦𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ ∃𝑦(𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)))
41 df-eu 2611 . . 3 (∃!𝑥(𝑥𝐴𝜑) ↔ ∃𝑦𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦))
42 df-rex 3056 . . 3 (∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦) ↔ ∃𝑦(𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)))
4340, 41, 423bitr4i 292 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦))
441, 43bitri 264 1 (∃!𝑥𝐴 𝜑 ↔ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1630  wex 1853  [wsb 2046  wcel 2139  ∃!weu 2607  wral 3050  wrex 3051  ∃!wreu 3052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-cleq 2753  df-clel 2756  df-ral 3055  df-rex 3056  df-reu 3057
This theorem is referenced by:  reu3  3537  reu6i  3538  reu8  3543  xpf1o  8287  ufileu  21924  isppw2  25040  cusgrfilem2  26562  fgreu  29780  fcnvgreu  29781  fourierdlem50  40876
  Copyright terms: Public domain W3C validator