Theorem 1stnpr

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

	Ref	Expression
Assertion	1stnpr	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( 1st ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		1stval	⊢ ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 }
2		dmsnn0	⊢ ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )
3	2	biimpri	⊢ ( dom { 𝐴 } ≠ ∅ → 𝐴 ∈ ( V × V ) )
4	3	necon1bi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → dom { 𝐴 } = ∅ )
5	4	unieqd	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ dom { 𝐴 } = ∪ ∅ )
6		uni0	⊢ ∪ ∅ = ∅
7	5 6	eqtrdi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ dom { 𝐴 } = ∅ )
8	1 7	eqtrid	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( 1st ‘ 𝐴 ) = ∅ )