Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mo4 Structured version   Visualization version   GIF version

Theorem mo4 2546
 Description: "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
mo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
mo4 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem mo4
StepHypRef Expression
1 nfv 1883 . 2 𝑥𝜓
2 mo4.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2mo4f 2545 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521  ∃*wmo 2499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503 This theorem is referenced by:  eu4  2547  rmo4  3432  dffun3  5937  fun11  6001  brprcneu  6222  dff13  6552  mpt2fun  6804  caovmo  6913  wemoiso  7195  wemoiso2  7196  addsrmo  9932  mulsrmo  9933  summo  14492  prodmo  14710  hausflimi  21831  vitalilem3  23424  plyexmo  24113  tglineintmo  25582  ajmoi  27842  pjhthmo  28289  adjmo  28819  moel  29451  noprefixmo  31973  funtransport  32263  funray  32372  funline  32374  lineintmo  32389  cossssid4  34360  dffrege115  38589
 Copyright terms: Public domain W3C validator