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

Theorem euind 3023
Description: Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010.)
Hypotheses
Ref Expression
euind.1 B V
euind.2 (x = y → (φψ))
euind.3 (x = yA = B)
Assertion
Ref Expression
euind ((xy((φ ψ) → A = B) xφ) → ∃!zx(φz = A))
Distinct variable groups:   y,z,φ   x,z,ψ   y,A,z   x,B,z   x,y
Allowed substitution hints:   φ(x)   ψ(y)   A(x)   B(y)

Proof of Theorem euind
Dummy variable w is distinct from all other variables.
StepHypRef Expression
1 euind.2 . . . . . 6 (x = y → (φψ))
21cbvexv 2003 . . . . 5 (xφyψ)
3 euind.1 . . . . . . . . 9 B V
43isseti 2865 . . . . . . . 8 z z = B
54biantrur 492 . . . . . . 7 (ψ ↔ (z z = B ψ))
65exbii 1582 . . . . . 6 (yψy(z z = B ψ))
7 19.41v 1901 . . . . . . . 8 (z(z = B ψ) ↔ (z z = B ψ))
87exbii 1582 . . . . . . 7 (yz(z = B ψ) ↔ y(z z = B ψ))
9 excom 1741 . . . . . . 7 (yz(z = B ψ) ↔ zy(z = B ψ))
108, 9bitr3i 242 . . . . . 6 (y(z z = B ψ) ↔ zy(z = B ψ))
116, 10bitri 240 . . . . 5 (yψzy(z = B ψ))
122, 11bitri 240 . . . 4 (xφzy(z = B ψ))
13 eqeq2 2362 . . . . . . . . 9 (A = B → (z = Az = B))
1413imim2i 13 . . . . . . . 8 (((φ ψ) → A = B) → ((φ ψ) → (z = Az = B)))
15 bi2 189 . . . . . . . . . 10 ((z = Az = B) → (z = Bz = A))
1615imim2i 13 . . . . . . . . 9 (((φ ψ) → (z = Az = B)) → ((φ ψ) → (z = Bz = A)))
17 an31 775 . . . . . . . . . . 11 (((φ ψ) z = B) ↔ ((z = B ψ) φ))
1817imbi1i 315 . . . . . . . . . 10 ((((φ ψ) z = B) → z = A) ↔ (((z = B ψ) φ) → z = A))
19 impexp 433 . . . . . . . . . 10 ((((φ ψ) z = B) → z = A) ↔ ((φ ψ) → (z = Bz = A)))
20 impexp 433 . . . . . . . . . 10 ((((z = B ψ) φ) → z = A) ↔ ((z = B ψ) → (φz = A)))
2118, 19, 203bitr3i 266 . . . . . . . . 9 (((φ ψ) → (z = Bz = A)) ↔ ((z = B ψ) → (φz = A)))
2216, 21sylib 188 . . . . . . . 8 (((φ ψ) → (z = Az = B)) → ((z = B ψ) → (φz = A)))
2314, 22syl 15 . . . . . . 7 (((φ ψ) → A = B) → ((z = B ψ) → (φz = A)))
24232alimi 1560 . . . . . 6 (xy((φ ψ) → A = B) → xy((z = B ψ) → (φz = A)))
25 19.23v 1891 . . . . . . . 8 (y((z = B ψ) → (φz = A)) ↔ (y(z = B ψ) → (φz = A)))
2625albii 1566 . . . . . . 7 (xy((z = B ψ) → (φz = A)) ↔ x(y(z = B ψ) → (φz = A)))
27 19.21v 1890 . . . . . . 7 (x(y(z = B ψ) → (φz = A)) ↔ (y(z = B ψ) → x(φz = A)))
2826, 27bitri 240 . . . . . 6 (xy((z = B ψ) → (φz = A)) ↔ (y(z = B ψ) → x(φz = A)))
2924, 28sylib 188 . . . . 5 (xy((φ ψ) → A = B) → (y(z = B ψ) → x(φz = A)))
3029eximdv 1622 . . . 4 (xy((φ ψ) → A = B) → (zy(z = B ψ) → zx(φz = A)))
3112, 30syl5bi 208 . . 3 (xy((φ ψ) → A = B) → (xφzx(φz = A)))
3231imp 418 . 2 ((xy((φ ψ) → A = B) xφ) → zx(φz = A))
33 pm4.24 624 . . . . . . . 8 (φ ↔ (φ φ))
3433biimpi 186 . . . . . . 7 (φ → (φ φ))
35 prth 554 . . . . . . 7 (((φz = A) (φw = A)) → ((φ φ) → (z = A w = A)))
36 eqtr3 2372 . . . . . . 7 ((z = A w = A) → z = w)
3734, 35, 36syl56 30 . . . . . 6 (((φz = A) (φw = A)) → (φz = w))
3837alanimi 1562 . . . . 5 ((x(φz = A) x(φw = A)) → x(φz = w))
39 19.23v 1891 . . . . . . 7 (x(φz = w) ↔ (xφz = w))
4039biimpi 186 . . . . . 6 (x(φz = w) → (xφz = w))
4140com12 27 . . . . 5 (xφ → (x(φz = w) → z = w))
4238, 41syl5 28 . . . 4 (xφ → ((x(φz = A) x(φw = A)) → z = w))
4342alrimivv 1632 . . 3 (xφzw((x(φz = A) x(φw = A)) → z = w))
4443adantl 452 . 2 ((xy((φ ψ) → A = B) xφ) → zw((x(φz = A) x(φw = A)) → z = w))
45 eqeq1 2359 . . . . 5 (z = w → (z = Aw = A))
4645imbi2d 307 . . . 4 (z = w → ((φz = A) ↔ (φw = A)))
4746albidv 1625 . . 3 (z = w → (x(φz = A) ↔ x(φw = A)))
4847eu4 2243 . 2 (∃!zx(φz = A) ↔ (zx(φz = A) zw((x(φz = A) x(φw = A)) → z = w)))
4932, 44, 48sylanbrc 645 1 ((xy((φ ψ) → A = B) xφ) → ∃!zx(φz = A))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  ∃!weu 2204  Vcvv 2859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator