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

Theorem riotaexg 5797
Description: Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
Assertion
Ref Expression
riotaexg (𝐴𝑉 → (𝑥𝐴 𝜓) ∈ V)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem riotaexg
StepHypRef Expression
1 df-riota 5793 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
2 uniexg 4412 . . 3 (𝐴𝑉 𝐴 ∈ V)
3 iotass 5165 . . . . 5 (∀𝑥((𝑥𝐴𝜓) → 𝑥 𝐴) → (℩𝑥(𝑥𝐴𝜓)) ⊆ 𝐴)
4 elssuni 3812 . . . . . 6 (𝑥𝐴𝑥 𝐴)
54adantr 274 . . . . 5 ((𝑥𝐴𝜓) → 𝑥 𝐴)
63, 5mpg 1438 . . . 4 (℩𝑥(𝑥𝐴𝜓)) ⊆ 𝐴
76a1i 9 . . 3 (𝐴𝑉 → (℩𝑥(𝑥𝐴𝜓)) ⊆ 𝐴)
82, 7ssexd 4117 . 2 (𝐴𝑉 → (℩𝑥(𝑥𝐴𝜓)) ∈ V)
91, 8eqeltrid 2251 1 (𝐴𝑉 → (𝑥𝐴 𝜓) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 2135  Vcvv 2722  wss 3112   cuni 3784  cio 5146  crio 5792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4095  ax-un 4406
This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2724  df-un 3116  df-in 3118  df-ss 3125  df-pw 3556  df-sn 3577  df-pr 3578  df-uni 3785  df-iota 5148  df-riota 5793
This theorem is referenced by:  flval  10198  sqrtrval  10932  qnumval  12106  qdenval  12107
  Copyright terms: Public domain W3C validator