### Nuprl Lemma : bor_wf

`∀[p,q:𝔹].  (p ∨bq ∈ 𝔹)`

Proof

Definitions occuring in Statement :  bor: `p ∨bq` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bor: `p ∨bq` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` prop: `ℙ`
Lemmas referenced :  bool_wf eqtt_to_assert btrue_wf uiff_transitivity equal-wf-T-base assert_wf bnot_wf not_wf eqff_to_assert assert_of_bnot equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule hypothesisEquality thin extract_by_obid hypothesis lambdaFormation sqequalHypSubstitution unionElimination equalityElimination isectElimination because_Cache productElimination independent_isectElimination baseClosed independent_functionElimination equalityTransitivity equalitySymmetry dependent_functionElimination axiomEquality Error :inhabitedIsType,  isect_memberEquality Error :universeIsType

Latex:
\mforall{}[p,q:\mBbbB{}].    (p  \mvee{}\msubb{}q  \mmember{}  \mBbbB{})

Date html generated: 2019_06_20-AM-11_30_59
Last ObjectModification: 2018_09_26-AM-11_13_39

Theory : bool_1

Home Index