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

Theorem mob 3653
Description: Equality implied by "at most one". (Contributed by NM, 18-Feb-2006.)
Hypotheses
Ref Expression
moi.1 (𝑥 = 𝐴 → (𝜑𝜓))
moi.2 (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
mob (((𝐴𝐶𝐵𝐷) ∧ ∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜒,𝑥   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mob
StepHypRef Expression
1 elex 3449 . . . . 5 (𝐵𝐷𝐵 ∈ V)
2 nfv 1917 . . . . . . . . . 10 𝑥 𝐵 ∈ V
3 nfmo1 2557 . . . . . . . . . 10 𝑥∃*𝑥𝜑
4 nfv 1917 . . . . . . . . . 10 𝑥𝜓
52, 3, 4nf3an 1904 . . . . . . . . 9 𝑥(𝐵 ∈ V ∧ ∃*𝑥𝜑𝜓)
6 nfv 1917 . . . . . . . . 9 𝑥(𝐴 = 𝐵𝜒)
75, 6nfim 1899 . . . . . . . 8 𝑥((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒))
8 moi.1 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝜑𝜓))
983anbi3d 1441 . . . . . . . . 9 (𝑥 = 𝐴 → ((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜑) ↔ (𝐵 ∈ V ∧ ∃*𝑥𝜑𝜓)))
10 eqeq1 2742 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
1110bibi1d 344 . . . . . . . . 9 (𝑥 = 𝐴 → ((𝑥 = 𝐵𝜒) ↔ (𝐴 = 𝐵𝜒)))
129, 11imbi12d 345 . . . . . . . 8 (𝑥 = 𝐴 → (((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜑) → (𝑥 = 𝐵𝜒)) ↔ ((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒))))
13 moi.2 . . . . . . . . 9 (𝑥 = 𝐵 → (𝜑𝜒))
1413mob2 3651 . . . . . . . 8 ((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜑) → (𝑥 = 𝐵𝜒))
157, 12, 14vtoclg1f 3503 . . . . . . 7 (𝐴𝐶 → ((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒)))
1615com12 32 . . . . . 6 ((𝐵 ∈ V ∧ ∃*𝑥𝜑𝜓) → (𝐴𝐶 → (𝐴 = 𝐵𝜒)))
17163expib 1121 . . . . 5 (𝐵 ∈ V → ((∃*𝑥𝜑𝜓) → (𝐴𝐶 → (𝐴 = 𝐵𝜒))))
181, 17syl 17 . . . 4 (𝐵𝐷 → ((∃*𝑥𝜑𝜓) → (𝐴𝐶 → (𝐴 = 𝐵𝜒))))
1918com3r 87 . . 3 (𝐴𝐶 → (𝐵𝐷 → ((∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒))))
2019imp 407 . 2 ((𝐴𝐶𝐵𝐷) → ((∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒)))
21203impib 1115 1 (((𝐴𝐶𝐵𝐷) ∧ ∃*𝑥𝜑𝜓) → (𝐴 = 𝐵𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  ∃*wmo 2538  Vcvv 3431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433
This theorem is referenced by:  moi  3654  rmob  3824
  Copyright terms: Public domain W3C validator