New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mo GIF version

Theorem mo 2226
 Description: Equivalent definitions of "there exists at most one." (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
Hypothesis
Ref Expression
mo.1 yφ
Assertion
Ref Expression
mo (yx(φx = y) ↔ xy((φ [y / x]φ) → x = y))
Distinct variable group:   x,y
Allowed substitution hints:   φ(x,y)

Proof of Theorem mo
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 mo.1 . . . . . 6 yφ
2 nfv 1619 . . . . . 6 y x = z
31, 2nfim 1813 . . . . 5 y(φx = z)
43nfal 1842 . . . 4 yx(φx = z)
5 nfv 1619 . . . 4 zx(φx = y)
6 equequ2 1686 . . . . . 6 (z = y → (x = zx = y))
76imbi2d 307 . . . . 5 (z = y → ((φx = z) ↔ (φx = y)))
87albidv 1625 . . . 4 (z = y → (x(φx = z) ↔ x(φx = y)))
94, 5, 8cbvex 1985 . . 3 (zx(φx = z) ↔ yx(φx = y))
101nfs1 2044 . . . . . . . . 9 x[y / x]φ
11 nfv 1619 . . . . . . . . 9 x y = z
1210, 11nfim 1813 . . . . . . . 8 x([y / x]φy = z)
13 sbequ2 1650 . . . . . . . . 9 (x = y → ([y / x]φφ))
14 ax-8 1675 . . . . . . . . 9 (x = y → (x = zy = z))
1513, 14imim12d 68 . . . . . . . 8 (x = y → ((φx = z) → ([y / x]φy = z)))
163, 12, 15cbv3 1982 . . . . . . 7 (x(φx = z) → y([y / x]φy = z))
1716ancli 534 . . . . . 6 (x(φx = z) → (x(φx = z) y([y / x]φy = z)))
183, 12aaan 1884 . . . . . 6 (xy((φx = z) ([y / x]φy = z)) ↔ (x(φx = z) y([y / x]φy = z)))
1917, 18sylibr 203 . . . . 5 (x(φx = z) → xy((φx = z) ([y / x]φy = z)))
20 prth 554 . . . . . . 7 (((φx = z) ([y / x]φy = z)) → ((φ [y / x]φ) → (x = z y = z)))
21 equtr2 1688 . . . . . . 7 ((x = z y = z) → x = y)
2220, 21syl6 29 . . . . . 6 (((φx = z) ([y / x]φy = z)) → ((φ [y / x]φ) → x = y))
23222alimi 1560 . . . . 5 (xy((φx = z) ([y / x]φy = z)) → xy((φ [y / x]φ) → x = y))
2419, 23syl 15 . . . 4 (x(φx = z) → xy((φ [y / x]φ) → x = y))
2524exlimiv 1634 . . 3 (zx(φx = z) → xy((φ [y / x]φ) → x = y))
269, 25sylbir 204 . 2 (yx(φx = y) → xy((φ [y / x]φ) → x = y))
27 nfa2 1855 . . . 4 yxy((φ [y / x]φ) → x = y)
28 sp 1747 . . . . . . . 8 (y((φ [y / x]φ) → x = y) → ((φ [y / x]φ) → x = y))
2928exp3a 425 . . . . . . 7 (y((φ [y / x]φ) → x = y) → (φ → ([y / x]φx = y)))
3029com3r 73 . . . . . 6 ([y / x]φ → (y((φ [y / x]φ) → x = y) → (φx = y)))
3110, 30alimd 1764 . . . . 5 ([y / x]φ → (xy((φ [y / x]φ) → x = y) → x(φx = y)))
3231com12 27 . . . 4 (xy((φ [y / x]φ) → x = y) → ([y / x]φx(φx = y)))
3327, 32eximd 1770 . . 3 (xy((φ [y / x]φ) → x = y) → (y[y / x]φyx(φx = y)))
34 alnex 1543 . . . 4 (y ¬ [y / x]φ ↔ ¬ y[y / x]φ)
3510nfn 1793 . . . . . 6 x ¬ [y / x]φ
361nfn 1793 . . . . . 6 y ¬ φ
37 sbequ1 1918 . . . . . . . 8 (x = y → (φ → [y / x]φ))
3837equcoms 1681 . . . . . . 7 (y = x → (φ → [y / x]φ))
3938con3d 125 . . . . . 6 (y = x → (¬ [y / x]φ → ¬ φ))
4035, 36, 39cbv3 1982 . . . . 5 (y ¬ [y / x]φx ¬ φ)
41 pm2.21 100 . . . . . 6 φ → (φx = y))
4241alimi 1559 . . . . 5 (x ¬ φx(φx = y))
43 19.8a 1756 . . . . 5 (x(φx = y) → yx(φx = y))
4440, 42, 433syl 18 . . . 4 (y ¬ [y / x]φyx(φx = y))
4534, 44sylbir 204 . . 3 y[y / x]φyx(φx = y))
4633, 45pm2.61d1 151 . 2 (xy((φ [y / x]φ) → x = y) → yx(φx = y))
4726, 46impbii 180 1 (yx(φx = y) ↔ xy((φ [y / x]φ) → x = y))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544   = wceq 1642  [wsb 1648 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649 This theorem is referenced by:  eu2  2229  eu3  2230  mo3  2235
 Copyright terms: Public domain W3C validator