Theorem f1preimaex

Description: If the image under a one-to-one function exists, then the corresponding preimage also exists. (Contributed by BTernaryTau, 21-Jun-2026)

	Ref	Expression
Assertion	f1preimaex	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ ( 𝐹 “ 𝐶 ) ∈ 𝑉 ) → 𝐶 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
2	1	simprbi	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ 𝐹 )
3		funimaexg	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 “ 𝐶 ) ∈ 𝑉 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) ∈ V )
4	2 3	sylan	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐹 “ 𝐶 ) ∈ 𝑉 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) ∈ V )
5	4	3adant2	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ ( 𝐹 “ 𝐶 ) ∈ 𝑉 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) ∈ V )
6		f1imacnv	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )
7	6	eleq1d	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) ∈ V ↔ 𝐶 ∈ V ) )
8	7	3adant3	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ ( 𝐹 “ 𝐶 ) ∈ 𝑉 ) → ( ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) ∈ V ↔ 𝐶 ∈ V ) )
9	5 8	mpbid	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ ( 𝐹 “ 𝐶 ) ∈ 𝑉 ) → 𝐶 ∈ V )