Theorem f10d

Description: The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020)

	Ref	Expression
Hypothesis	f10d.f	⊢ ( 𝜑 → 𝐹 = ∅ )
Assertion	f10d	⊢ ( 𝜑 → 𝐹 : dom 𝐹 –1-1→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		f10d.f	⊢ ( 𝜑 → 𝐹 = ∅ )
2		f10	⊢ ∅ : ∅ –1-1→ 𝐴
3		dm0	⊢ dom ∅ = ∅
4		f1eq2	⊢ ( dom ∅ = ∅ → ( ∅ : dom ∅ –1-1→ 𝐴 ↔ ∅ : ∅ –1-1→ 𝐴 ) )
5	3 4	ax-mp	⊢ ( ∅ : dom ∅ –1-1→ 𝐴 ↔ ∅ : ∅ –1-1→ 𝐴 )
6	2 5	mpbir	⊢ ∅ : dom ∅ –1-1→ 𝐴
7	1	dmeqd	⊢ ( 𝜑 → dom 𝐹 = dom ∅ )
8		eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )
9	1 7 8	f1eq123d	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 –1-1→ 𝐴 ↔ ∅ : dom ∅ –1-1→ 𝐴 ) )
10	6 9	mpbiri	⊢ ( 𝜑 → 𝐹 : dom 𝐹 –1-1→ 𝐴 )