This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpoxopx0ov0

Description: If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017)

		Ref	Expression
	Hypothesis	mpoxopn0yelv.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1^st ‘ 𝑥 ) ↦ 𝐶 )
	Assertion	mpoxopx0ov0	⊢ ( ∅ 𝐹 𝐾 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		mpoxopn0yelv.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1^st ‘ 𝑥 ) ↦ 𝐶 )
2		0nelxp	⊢ ¬ ∅ ∈ ( V × V )
3	1	mpoxopxnop0	⊢ ( ¬ ∅ ∈ ( V × V ) → ( ∅ 𝐹 𝐾 ) = ∅ )
4	2 3	ax-mp	⊢ ( ∅ 𝐹 𝐾 ) = ∅