ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mo4 Unicode version

Theorem mo4 2099
Description: "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
mo4.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
mo4  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Distinct variable groups:    x, y    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem mo4
StepHypRef Expression
1 nfv 1539 . 2  |-  F/ x ps
2 mo4.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
31, 2mo4f 2098 1  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105   A.wal 1362   E*wmo 2039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042
This theorem is referenced by:  eu4  2100  rmo4  2945  dffun5r  5243  dffun6f  5244  fun11  5298  brprcneu  5523  dff13  5785  mpofun  5993  caovimo  6085  th3qlem1  6655  exmidmotap  7278  addnq0mo  7464  mulnq0mo  7465  addsrmo  7760  mulsrmo  7761  summodc  11409  prodmodc  11604  limcimo  14531
  Copyright terms: Public domain W3C validator