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

Theorem mob2 2715
Description: Consequence of "at most one." (Contributed by NM, 2-Jan-2015.)
Hypothesis
Ref Expression
moi2.1 (x = A → (φψ))
Assertion
Ref Expression
mob2 ((A B ∃*xφ φ) → (x = Aψ))
Distinct variable groups:   x,A   ψ,x
Allowed substitution hints:   φ(x)   B(x)

Proof of Theorem mob2
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 simp3 905 . . 3 ((A B ∃*xφ φ) → φ)
2 moi2.1 . . 3 (x = A → (φψ))
31, 2syl5ibcom 144 . 2 ((A B ∃*xφ φ) → (x = Aψ))
4 nfs1v 1812 . . . . . . . 8 x[y / x]φ
5 sbequ12 1651 . . . . . . . 8 (x = y → (φ ↔ [y / x]φ))
64, 5mo4f 1957 . . . . . . 7 (∃*xφxy((φ [y / x]φ) → x = y))
7 sp 1398 . . . . . . 7 (xy((φ [y / x]φ) → x = y) → y((φ [y / x]φ) → x = y))
86, 7sylbi 114 . . . . . 6 (∃*xφy((φ [y / x]φ) → x = y))
9 nfv 1418 . . . . . . . . . 10 xψ
109, 2sbhypf 2597 . . . . . . . . 9 (y = A → ([y / x]φψ))
1110anbi2d 437 . . . . . . . 8 (y = A → ((φ [y / x]φ) ↔ (φ ψ)))
12 eqeq2 2046 . . . . . . . 8 (y = A → (x = yx = A))
1311, 12imbi12d 223 . . . . . . 7 (y = A → (((φ [y / x]φ) → x = y) ↔ ((φ ψ) → x = A)))
1413spcgv 2634 . . . . . 6 (A B → (y((φ [y / x]φ) → x = y) → ((φ ψ) → x = A)))
158, 14syl5 28 . . . . 5 (A B → (∃*xφ → ((φ ψ) → x = A)))
1615imp 115 . . . 4 ((A B ∃*xφ) → ((φ ψ) → x = A))
1716expd 245 . . 3 ((A B ∃*xφ) → (φ → (ψx = A)))
18173impia 1100 . 2 ((A B ∃*xφ φ) → (ψx = A))
193, 18impbid 120 1 ((A B ∃*xφ φ) → (x = Aψ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 884  wal 1240   = wceq 1242   wcel 1390  [wsb 1642  ∃*wmo 1898
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-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553
This theorem is referenced by:  moi2  2716  mob  2717
  Copyright terms: Public domain W3C validator