Nuprl Rule : isect_memberFormation
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ ⋂x:A. B ext b
BY isect_memberFormation !parameter{i:l} z ()
H [z:A] ⊢ B[z/x] ext b
H ⊢ A = A ∈ Type
Definitions occuring in rule :
isect: ⋂x:A. B[x],
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H \mvdash{} \mcap{}x:A. B ext b
BY isect\_memberFormation !parameter\{i:l\} z ()
H [z:A] \mvdash{} B[z/x] ext b
H \mvdash{} A = A
Date html generated:
2019_06_20-PM-04_11_50
Last ObjectModification:
2018_09_25-PM-01_39_08
Theory : rules
Home
Index