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 5686 proves that it does this. For example, (2^{nd} ‘⟨ 3 , 4 ⟩) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 4721 and op2ndb 4720). 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 5678  . 2 class 2^{nd}  
2  vx  . . 3 setvar x  
3  cvv 2527  . . 3 class V  
4  2  cv 1223  . . . . . 6 class x 
5  4  csn 3340  . . . . 5 class {x} 
6  5  crn 4262  . . . 4 class ran {x} 
7  6  cuni 3544  . . 3 class ∪ ran {x} 
8  2, 3, 7  cmpt 3782  . 2 class (x ∈ V ↦ ∪ ran {x}) 
9  1, 8  wceq 1224  1 wff 2^{nd} = (x ∈ V ↦ ∪ ran {x}) 
Colors of variables: wff set class 
This definition is referenced by: 2ndvalg 5682 fo2nd 5697 f2ndres 5699 
Copyright terms: Public domain  W3C validator 