Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > df2nd  Structured version GIF version 
Description: Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 5716 proves that it does this. For example, (2^{nd} ‘⟨ 3 , 4 ⟩) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 4748 and op2ndb 4747). The notation is the same as Monk's. (Contributed by NM, 9Oct2004.) 
Ref  Expression 

df2nd  ⊢ 2^{nd} = (x ∈ V ↦ ∪ ran {x}) 
Step  Hyp  Ref  Expression 

1  c2nd 5708  . 2 class 2^{nd}  
2  vx  . . 3 setvar x  
3  cvv 2551  . . 3 class V  
4  2  cv 1241  . . . . . 6 class x 
5  4  csn 3367  . . . . 5 class {x} 
6  5  crn 4289  . . . 4 class ran {x} 
7  6  cuni 3571  . . 3 class ∪ ran {x} 
8  2, 3, 7  cmpt 3809  . 2 class (x ∈ V ↦ ∪ ran {x}) 
9  1, 8  wceq 1242  1 wff 2^{nd} = (x ∈ V ↦ ∪ ran {x}) 
Colors of variables: wff set class 
This definition is referenced by: 2ndvalg 5712 fo2nd 5727 f2ndres 5729 
Copyright terms: Public domain  W3C validator 