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

Theorem iotam 5208
Description: Representation of "the unique element such that 𝜑 " with a class expression 𝐴 which is inhabited (that means that "the unique element such that 𝜑 " exists). (Contributed by AV, 30-Jan-2024.)
Hypothesis
Ref Expression
iotam.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
iotam ((𝐴𝑉 ∧ ∃𝑤 𝑤𝐴𝐴 = (℩𝑥𝜑)) → 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑤,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑤)   𝜓(𝑤)   𝑉(𝑥,𝑤)

Proof of Theorem iotam
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eleq1w 2238 . . . . 5 (𝑤 = 𝑧 → (𝑤𝐴𝑧𝐴))
21cbvexv 1918 . . . 4 (∃𝑤 𝑤𝐴 ↔ ∃𝑧 𝑧𝐴)
3 simprr 531 . . . . . . . 8 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → 𝐴 = (℩𝑥𝜑))
43eqcomd 2183 . . . . . . 7 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → (℩𝑥𝜑) = 𝐴)
5 simprl 529 . . . . . . . 8 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → 𝐴𝑉)
6 simpl 109 . . . . . . . . . 10 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → 𝑧𝐴)
76, 3eleqtrd 2256 . . . . . . . . 9 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → 𝑧 ∈ (℩𝑥𝜑))
8 eliotaeu 5205 . . . . . . . . 9 (𝑧 ∈ (℩𝑥𝜑) → ∃!𝑥𝜑)
97, 8syl 14 . . . . . . . 8 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → ∃!𝑥𝜑)
10 iotam.1 . . . . . . . . 9 (𝑥 = 𝐴 → (𝜑𝜓))
1110iota2 5206 . . . . . . . 8 ((𝐴𝑉 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))
125, 9, 11syl2anc 411 . . . . . . 7 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))
134, 12mpbird 167 . . . . . 6 ((𝑧𝐴 ∧ (𝐴𝑉𝐴 = (℩𝑥𝜑))) → 𝜓)
1413ex 115 . . . . 5 (𝑧𝐴 → ((𝐴𝑉𝐴 = (℩𝑥𝜑)) → 𝜓))
1514exlimiv 1598 . . . 4 (∃𝑧 𝑧𝐴 → ((𝐴𝑉𝐴 = (℩𝑥𝜑)) → 𝜓))
162, 15sylbi 121 . . 3 (∃𝑤 𝑤𝐴 → ((𝐴𝑉𝐴 = (℩𝑥𝜑)) → 𝜓))
17163impib 1201 . 2 ((∃𝑤 𝑤𝐴𝐴𝑉𝐴 = (℩𝑥𝜑)) → 𝜓)
18173com12 1207 1 ((𝐴𝑉 ∧ ∃𝑤 𝑤𝐴𝐴 = (℩𝑥𝜑)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wex 1492  ∃!weu 2026  wcel 2148  cio 5176
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-sn 3598  df-pr 3599  df-uni 3810  df-iota 5178
This theorem is referenced by:  sgrpidmndm  12820
  Copyright terms: Public domain W3C validator