Theorem mo4 2141

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

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
2		mo4.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	mo4f 2140	1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1395  ∃*wmo 2080

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083

This theorem is referenced by:  eu4  2142  rmo4  2999  dffun5r  5338  dffun6f  5339  fun11  5397  brprcneu  5632  dff13  5908  mpofun  6122  caovimo  6215  th3qlem1  6805  exmidmotap  7479  addnq0mo  7666  mulnq0mo  7667  addsrmo  7962  mulsrmo  7963  summodc  11943  prodmodc  12138  limcimo  15388