ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  euind Structured version   GIF version

Theorem euind 2722
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 1792 . . . . 5 (xφyψ)
3 euind.1 . . . . . . . . 9 B V
43isseti 2557 . . . . . . . 8 z z = B
54biantrur 287 . . . . . . 7 (ψ ↔ (z z = B ψ))
65exbii 1493 . . . . . 6 (yψy(z z = B ψ))
7 19.41v 1779 . . . . . . 7 (z(z = B ψ) ↔ (z z = B ψ))
87exbii 1493 . . . . . 6 (yz(z = B ψ) ↔ y(z z = B ψ))
9 excom 1551 . . . . . 6 (yz(z = B ψ) ↔ zy(z = B ψ))
106, 8, 93bitr2i 197 . . . . 5 (yψzy(z = B ψ))
112, 10bitri 173 . . . 4 (xφzy(z = B ψ))
12 eqeq2 2046 . . . . . . . . 9 (A = B → (z = Az = B))
1312imim2i 12 . . . . . . . 8 (((φ ψ) → A = B) → ((φ ψ) → (z = Az = B)))
14 bi2 121 . . . . . . . . . 10 ((z = Az = B) → (z = Bz = A))
1514imim2i 12 . . . . . . . . 9 (((φ ψ) → (z = Az = B)) → ((φ ψ) → (z = Bz = A)))
16 an31 498 . . . . . . . . . . 11 (((φ ψ) z = B) ↔ ((z = B ψ) φ))
1716imbi1i 227 . . . . . . . . . 10 ((((φ ψ) z = B) → z = A) ↔ (((z = B ψ) φ) → z = A))
18 impexp 250 . . . . . . . . . 10 ((((φ ψ) z = B) → z = A) ↔ ((φ ψ) → (z = Bz = A)))
19 impexp 250 . . . . . . . . . 10 ((((z = B ψ) φ) → z = A) ↔ ((z = B ψ) → (φz = A)))
2017, 18, 193bitr3i 199 . . . . . . . . 9 (((φ ψ) → (z = Bz = A)) ↔ ((z = B ψ) → (φz = A)))
2115, 20sylib 127 . . . . . . . 8 (((φ ψ) → (z = Az = B)) → ((z = B ψ) → (φz = A)))
2213, 21syl 14 . . . . . . 7 (((φ ψ) → A = B) → ((z = B ψ) → (φz = A)))
23222alimi 1342 . . . . . 6 (xy((φ ψ) → A = B) → xy((z = B ψ) → (φz = A)))
24 19.23v 1760 . . . . . . . 8 (y((z = B ψ) → (φz = A)) ↔ (y(z = B ψ) → (φz = A)))
2524albii 1356 . . . . . . 7 (xy((z = B ψ) → (φz = A)) ↔ x(y(z = B ψ) → (φz = A)))
26 19.21v 1750 . . . . . . 7 (x(y(z = B ψ) → (φz = A)) ↔ (y(z = B ψ) → x(φz = A)))
2725, 26bitri 173 . . . . . 6 (xy((z = B ψ) → (φz = A)) ↔ (y(z = B ψ) → x(φz = A)))
2823, 27sylib 127 . . . . 5 (xy((φ ψ) → A = B) → (y(z = B ψ) → x(φz = A)))
2928eximdv 1757 . . . 4 (xy((φ ψ) → A = B) → (zy(z = B ψ) → zx(φz = A)))
3011, 29syl5bi 141 . . 3 (xy((φ ψ) → A = B) → (xφzx(φz = A)))
3130imp 115 . 2 ((xy((φ ψ) → A = B) xφ) → zx(φz = A))
32 pm4.24 375 . . . . . . . 8 (φ ↔ (φ φ))
3332biimpi 113 . . . . . . 7 (φ → (φ φ))
34 prth 326 . . . . . . 7 (((φz = A) (φw = A)) → ((φ φ) → (z = A w = A)))
35 eqtr3 2056 . . . . . . 7 ((z = A w = A) → z = w)
3633, 34, 35syl56 30 . . . . . 6 (((φz = A) (φw = A)) → (φz = w))
3736alanimi 1345 . . . . 5 ((x(φz = A) x(φw = A)) → x(φz = w))
38 19.23v 1760 . . . . . . 7 (x(φz = w) ↔ (xφz = w))
3938biimpi 113 . . . . . 6 (x(φz = w) → (xφz = w))
4039com12 27 . . . . 5 (xφ → (x(φz = w) → z = w))
4137, 40syl5 28 . . . 4 (xφ → ((x(φz = A) x(φw = A)) → z = w))
4241alrimivv 1752 . . 3 (xφzw((x(φz = A) x(φw = A)) → z = w))
4342adantl 262 . 2 ((xy((φ ψ) → A = B) xφ) → zw((x(φz = A) x(φw = A)) → z = w))
44 eqeq1 2043 . . . . 5 (z = w → (z = Aw = A))
4544imbi2d 219 . . . 4 (z = w → ((φz = A) ↔ (φw = A)))
4645albidv 1702 . . 3 (z = w → (x(φz = A) ↔ x(φw = A)))
4746eu4 1959 . 2 (∃!zx(φz = A) ↔ (zx(φz = A) zw((x(φz = A) x(φw = A)) → z = w)))
4831, 43, 47sylanbrc 394 1 ((xy((φ ψ) → A = B) xφ) → ∃!zx(φz = A))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1240   = wceq 1242  wex 1378   wcel 1390  ∃!weu 1897  Vcvv 2551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator