Metamath Proof Explorer


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