Theorem imaeqsexv

Description: Substitute a function value into an existential quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024)

	Ref	Expression
Hypothesis	imaeqsex.1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	imaeqsexv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		imaeqsex.1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
2		df-rex	⊢ ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ∧ 𝜑 ) )
3		fvelimab	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
4	3	anbi1d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ) )
5	4	exbidv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ) )
6	2 5	syl5bb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ) )
7		rexcom4	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) )
8		eqcom	⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑦 ) )
9	8	anbi1i	⊢ ( ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ∧ 𝜑 ) )
10	9	exbii	⊢ ( ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ∧ 𝜑 ) )
11		fvex	⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
12	11 1	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ∧ 𝜑 ) ↔ 𝜓 )
13	10 12	bitri	⊢ ( ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ 𝜓 )
14	13	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 𝜓 )
15		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) )
16	15	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) )
17	7 14 16	3bitr3ri	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 𝜓 )
18	6 17	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) )