Theorem ralrnmpt3

Description: A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	ralrnmpt3.1	⊢ Ⅎ 𝑥 𝜑
	ralrnmpt3.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	ralrnmpt3.3	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
Assertion	ralrnmpt3	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralrnmpt3.1	⊢ Ⅎ 𝑥 𝜑
2		ralrnmpt3.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		ralrnmpt3.3	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
4	1 2	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	5 3	ralrnmptw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
7	4 6	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) )