Theorem 2ndval2

Description: Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

	Ref	Expression
Assertion	2ndval2	⊢ ( 𝐴 ∈ ( V × V ) → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		elvv	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	op2nd	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
5	2 3	op2ndb	⊢ ∩ ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } = 𝑦
6	4 5	eqtr4i	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ∩ ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ }
7		fveq2	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8		sneq	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
9	8	cnveqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ◡ { 𝐴 } = ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
10	9	inteqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ◡ { 𝐴 } = ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
11	10	inteqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ ◡ { 𝐴 } = ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
12	11	inteqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ ∩ ◡ { 𝐴 } = ∩ ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
13	6 7 12	3eqtr4a	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )
14	13	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )
15	1 14	sylbi	⊢ ( 𝐴 ∈ ( V × V ) → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )