Nuprl Rule : existsFunctionality

H p:(∃x1:T. P) @lvl, J ⊢ ∃x2:T. Q ext let v,w = p in <v, t>

  BY existsFunctionality #$i v w ()

  H v:T @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t
  H v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Latex:
H p:(\mexists{}x1:T. P) @lvl, J \mvdash{} \mexists{}x2:T. Q ext let v,w = p in <v, t> BY existsFunctionality \#\$i v w () H v:T @lvl, w:P[v/x1] @lvl, J \mvdash{} Q[v/x2] ext t H v:T @lvl, w:P \mmember{} \mBbbU{}\{lvl\}[v/x1], J \mvdash{} Q \mmember{} \mBbbU{}\{lvl\}[v/x2] Date html generated: 2019_06_20-PM-04_11_53 Last ObjectModification: 2016_01_12-PM-01_16_32 Theory : rules Home Index