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

Theorem iota4 5831
Description: Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
Assertion
Ref Expression
iota4 (∃!𝑥𝜑[(℩𝑥𝜑) / 𝑥]𝜑)

Proof of Theorem iota4
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-eu 2478 . 2 (∃!𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
2 biimpr 210 . . . . . 6 ((𝜑𝑥 = 𝑧) → (𝑥 = 𝑧𝜑))
32alimi 1736 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥(𝑥 = 𝑧𝜑))
4 sb2 2356 . . . . 5 (∀𝑥(𝑥 = 𝑧𝜑) → [𝑧 / 𝑥]𝜑)
53, 4syl 17 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → [𝑧 / 𝑥]𝜑)
6 iotaval 5824 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑧) → (℩𝑥𝜑) = 𝑧)
76eqcomd 2632 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → 𝑧 = (℩𝑥𝜑))
8 dfsbcq2 3425 . . . . 5 (𝑧 = (℩𝑥𝜑) → ([𝑧 / 𝑥]𝜑[(℩𝑥𝜑) / 𝑥]𝜑))
97, 8syl 17 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → ([𝑧 / 𝑥]𝜑[(℩𝑥𝜑) / 𝑥]𝜑))
105, 9mpbid 222 . . 3 (∀𝑥(𝜑𝑥 = 𝑧) → [(℩𝑥𝜑) / 𝑥]𝜑)
1110exlimiv 1860 . 2 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → [(℩𝑥𝜑) / 𝑥]𝜑)
121, 11sylbi 207 1 (∃!𝑥𝜑[(℩𝑥𝜑) / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478   = wceq 1480  wex 1701  [wsb 1882  ∃!weu 2474  [wsbc 3422  cio 5811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rex 2918  df-v 3193  df-sbc 3423  df-un 3565  df-sn 4154  df-pr 4156  df-uni 4408  df-iota 5813
This theorem is referenced by:  iota4an  5832  iotacl  5836  pm14.24  38101  sbiota1  38103
  Copyright terms: Public domain W3C validator