Theorem f1setex

Description: The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024)

	Ref	Expression
Assertion	f1setex	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fsetex	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )
2		df-f1	⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) )
3	2	abbii	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) }
4		abanssl	⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
5	3 4	eqsstri	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
6	5	a1i	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } )
7	1 6	ssexd	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ∈ V )