Theorem 2ndnpr

Description: Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017)

	Ref	Expression
Assertion	2ndnpr	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( 2nd ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		2ndval	⊢ ( 2nd ‘ 𝐴 ) = ∪ ran { 𝐴 }
2		rnsnn0	⊢ ( 𝐴 ∈ ( V × V ) ↔ ran { 𝐴 } ≠ ∅ )
3	2	biimpri	⊢ ( ran { 𝐴 } ≠ ∅ → 𝐴 ∈ ( V × V ) )
4	3	necon1bi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ran { 𝐴 } = ∅ )
5	4	unieqd	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ ran { 𝐴 } = ∪ ∅ )
6		uni0	⊢ ∪ ∅ = ∅
7	5 6	syl6eq	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ ran { 𝐴 } = ∅ )
8	1 7	syl5eq	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( 2nd ‘ 𝐴 ) = ∅ )