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