Nuprl Rule : independent_pairEquality
H ⊢ <a1, b1> = <a2, b2> ∈ (A × B)
BY independent_pairEquality ()
H ⊢ a1 = a2 ∈ A
H ⊢ b1 = b2 ∈ B
Definitions occuring in rule :
product: x:A × B[x],
pair: <a, b>,
equal: s = t ∈ T,
axiom: Ax
Latex:
H \mvdash{} <a1, b1> = <a2, b2>
BY independent\_pairEquality ()
H \mvdash{} a1 = a2
H \mvdash{} b1 = b2
Date html generated:
2019_06_20-PM-04_11_45
Last ObjectModification:
2015_11_25-PM-03_37_46
Theory : rules
Home
Index