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

Theorem reu6 3362
 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 2903 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
2 19.28v 1896 . . . . 5 (∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ↔ (𝑦𝐴 ∧ ∀𝑥(𝑥𝐴 → (𝜑𝑥 = 𝑦))))
3 eleq1 2676 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
4 sbequ12 2097 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
53, 4anbi12d 743 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑)))
6 equequ1 1939 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑥 = 𝑦𝑦 = 𝑦))
75, 6bibi12d 334 . . . . . . . . . 10 (𝑥 = 𝑦 → (((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦)))
8 equid 1926 . . . . . . . . . . . 12 𝑦 = 𝑦
98tbt 358 . . . . . . . . . . 11 ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦))
10 simpl 472 . . . . . . . . . . 11 ((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦𝐴)
119, 10sylbir 224 . . . . . . . . . 10 (((𝑦𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦) → 𝑦𝐴)
127, 11syl6bi 242 . . . . . . . . 9 (𝑥 = 𝑦 → (((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → 𝑦𝐴))
1312spimv 2245 . . . . . . . 8 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → 𝑦𝐴)
14 ibar 524 . . . . . . . . . . 11 (𝑥𝐴 → (𝜑 ↔ (𝑥𝐴𝜑)))
1514bibi1d 332 . . . . . . . . . 10 (𝑥𝐴 → ((𝜑𝑥 = 𝑦) ↔ ((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦)))
1615biimprcd 239 . . . . . . . . 9 (((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → (𝑥𝐴 → (𝜑𝑥 = 𝑦)))
1716sps 2043 . . . . . . . 8 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → (𝑥𝐴 → (𝜑𝑥 = 𝑦)))
1813, 17jca 553 . . . . . . 7 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → (𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))))
1918axc4i 2116 . . . . . 6 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) → ∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))))
20 biimp 204 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
2120imim2i 16 . . . . . . . . . 10 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → (𝑥𝐴 → (𝜑𝑥 = 𝑦)))
2221impd 446 . . . . . . . . 9 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → ((𝑥𝐴𝜑) → 𝑥 = 𝑦))
2322adantl 481 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → ((𝑥𝐴𝜑) → 𝑥 = 𝑦))
24 eleq1a 2683 . . . . . . . . . . . 12 (𝑦𝐴 → (𝑥 = 𝑦𝑥𝐴))
2524adantr 480 . . . . . . . . . . 11 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → (𝑥 = 𝑦𝑥𝐴))
2625imp 444 . . . . . . . . . 10 (((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝑥𝐴)
27 biimpr 209 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
2827imim2i 16 . . . . . . . . . . . . 13 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → (𝑥𝐴 → (𝑥 = 𝑦𝜑)))
2928com23 84 . . . . . . . . . . . 12 ((𝑥𝐴 → (𝜑𝑥 = 𝑦)) → (𝑥 = 𝑦 → (𝑥𝐴𝜑)))
3029imp 444 . . . . . . . . . . 11 (((𝑥𝐴 → (𝜑𝑥 = 𝑦)) ∧ 𝑥 = 𝑦) → (𝑥𝐴𝜑))
3130adantll 746 . . . . . . . . . 10 (((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝑥𝐴𝜑))
3226, 31jcai 557 . . . . . . . . 9 (((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝑥𝐴𝜑))
3332ex 449 . . . . . . . 8 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → (𝑥 = 𝑦 → (𝑥𝐴𝜑)))
3423, 33impbid 201 . . . . . . 7 ((𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → ((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦))
3534alimi 1730 . . . . . 6 (∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))) → ∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦))
3619, 35impbii 198 . . . . 5 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(𝑦𝐴 ∧ (𝑥𝐴 → (𝜑𝑥 = 𝑦))))
37 df-ral 2901 . . . . . 6 (∀𝑥𝐴 (𝜑𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝑥 = 𝑦)))
3837anbi2i 726 . . . . 5 ((𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)) ↔ (𝑦𝐴 ∧ ∀𝑥(𝑥𝐴 → (𝜑𝑥 = 𝑦))))
392, 36, 383bitr4i 291 . . . 4 (∀𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ (𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)))
4039exbii 1764 . . 3 (∃𝑦𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦) ↔ ∃𝑦(𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)))
41 df-eu 2462 . . 3 (∃!𝑥(𝑥𝐴𝜑) ↔ ∃𝑦𝑥((𝑥𝐴𝜑) ↔ 𝑥 = 𝑦))
42 df-rex 2902 . . 3 (∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦) ↔ ∃𝑦(𝑦𝐴 ∧ ∀𝑥𝐴 (𝜑𝑥 = 𝑦)))
4340, 41, 423bitr4i 291 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦))
441, 43bitri 263 1 (∃!𝑥𝐴 𝜑 ↔ ∃𝑦𝐴𝑥𝐴 (𝜑𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695  [wsb 1867   ∈ wcel 1977  ∃!weu 2458  ∀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-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-cleq 2603  df-clel 2606  df-ral 2901  df-rex 2902  df-reu 2903 This theorem is referenced by:  reu3  3363  reu6i  3364  reu8  3369  xpf1o  8007  ufileu  21533  isppw2  24641  cusgrafilem2  26008  fgreu  28854  fcnvgreu  28855  fourierdlem50  39049  cusgrfilem2  40672
 Copyright terms: Public domain W3C validator