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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) |
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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) |