Nuprl Rule : existsLevelFunctionality

H x:(∃x1:T. P ∈ 𝕌{lvl}), J ⊢ ∃x2:T. Q ∈ 𝕌{lvl} ext experimental{existsLevelFunctionality}(Ax)

  BY existsLevelFunctionality #$i v w ()

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

Latex:
H x:(\mexists{}x1:T. P \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} \mexists{}x2:T. Q \mmember{} \mBbbU{}\{lvl\} ext experimental\{existsLevelFunctionality\}(Ax) BY existsLevelFunctionality \#\$i v w () 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_33 Theory : rules Home Index