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

Theorem riotabidv 5827
Description: Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
Hypothesis
Ref Expression
riotabidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
riotabidv (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem riotabidv
StepHypRef Expression
1 biidd 172 . . . 4 (𝜑 → (𝑥𝐴𝑥𝐴))
2 riotabidv.1 . . . 4 (𝜑 → (𝜓𝜒))
31, 2anbi12d 473 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
43iotabidv 5195 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
5 df-riota 5825 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
6 df-riota 5825 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
74, 5, 63eqtr4g 2235 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  cio 5172  crio 5824
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-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3808  df-iota 5174  df-riota 5825
This theorem is referenced by:  riotaeqbidv  5828  csbriotag  5837  infvalti  7015  caucvgsrlemfv  7778  axcaucvglemval  7884  axcaucvglemcau  7885  subval  8136  divvalap  8617  divfnzn  9607  flval  10255  cjval  10835  sqrtrval  10990  qnumval  12165  qdenval  12166  grpinvval  12803
  Copyright terms: Public domain W3C validator