Theorem ralima

Description: Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)

	Ref	Expression
Hypothesis	ralima.x	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ralima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ralima.x	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
2		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3	2	funfnd	⊢ ( 𝐹 Fn 𝐴 → 𝐹 Fn dom 𝐹 )
4		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
5	4	sseq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
6	5	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ dom 𝐹 )
7		fvexd	⊢ ( ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ V )
8		fvelimab	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
9		eqcom	⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑦 ) )
10	9	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
11	8 10	bitrdi	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝑥 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
12	1	adantl	⊢ ( ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜑 ↔ 𝜓 ) )
13	7 11 12	ralxfr2d	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )
14	3 6 13	syl2an2r	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 ) )