HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem mopick 1426
Description: "At most one" picks a variable value, eliminating an existential quantifier.
Assertion
Ref Expression
mopick |- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
Proof of Theorem mopick
StepHypRef Expression
1 ax-17 968 . . . 4 |- ((ph /\ ps) -> A.y(ph /\ ps))
2 hbs1 1327 . . . . 5 |- ([y / x]ph -> A.x[y / x]ph)
3 hbs1 1327 . . . . 5 |- ([y / x]ps -> A.x[y / x]ps)
42, 3hban 1006 . . . 4 |- (([y / x]ph /\ [y / x]ps) -> A.x([y / x]ph /\ [y / x]ps))
5 sbequ12 1177 . . . . 5 |- (x = y -> (ph <-> [y / x]ph))
6 sbequ12 1177 . . . . 5 |- (x = y -> (ps <-> [y / x]ps))
75, 6anbi12d 626 . . . 4 |- (x = y -> ((ph /\ ps) <-> ([y / x]ph /\ [y / x]ps)))
81, 4, 7cbvex 1162 . . 3 |- (E.x(ph /\ ps) <-> E.y([y / x]ph /\ [y / x]ps))
9 sbequ2 1175 . . . . . . . . 9 |- (x = y -> ([y / x]ps -> ps))
109imim2i 17 . . . . . . . 8 |- (((ph /\ [y / x]ph) -> x = y) -> ((ph /\ [y / x]ph) -> ([y / x]ps -> ps)))
1110exp3a 375 . . . . . . 7 |- (((ph /\ [y / x]ph) -> x = y) -> (ph -> ([y / x]ph -> ([y / x]ps -> ps))))
1211com4t 40 . . . . . 6 |- ([y / x]ph -> ([y / x]ps -> (((ph /\ [y / x]ph) -> x = y) -> (ph -> ps))))
1312imp 350 . . . . 5 |- (([y / x]ph /\ [y / x]ps) -> (((ph /\ [y / x]ph) -> x = y) -> (ph -> ps)))
14 ax-17 968 . . . . . . 7 |- (ph -> A.yph)
1514mo3 1394 . . . . . 6 |- (E*xph <-> A.xA.y((ph /\ [y / x]ph) -> x = y))
16 ax-4 970 . . . . . . 7 |- (A.y((ph /\ [y / x]ph) -> x = y) -> ((ph /\ [y / x]ph) -> x = y))
1716a4s 981 . . . . . 6 |- (A.xA.y((ph /\ [y / x]ph) -> x = y) -> ((ph /\ [y / x]ph) -> x = y))
1815, 17sylbi 199 . . . . 5 |- (E*xph -> ((ph /\ [y / x]ph) -> x = y))
1913, 18syl5 21 . . . 4 |- (([y / x]ph /\ [y / x]ps) -> (E*xph -> (ph -> ps)))
201919.23aiv 1290 . . 3 |- (E.y([y / x]ph /\ [y / x]ps) -> (E*xph -> (ph -> ps)))
218, 20sylbi 199 . 2 |- (E.x(ph /\ ps) -> (E*xph -> (ph -> ps)))
2221impcom 351 1 |- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223  A.wal 951  E.wex 977  E*wmo 1374
This theorem is referenced by:  eupick 1427  mopick2 1429  moexex 1431  imadif 3560
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376
Copyright terms: Public domain