# Metamath Proof Explorer

## Theorem ralrn

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013) (Revised by Mario Carneiro, 20-Aug-2014)

Ref Expression
Hypothesis rexrn.1 ${⊢}{x}={F}\left({y}\right)\to \left({\phi }↔{\psi }\right)$
Assertion ralrn ${⊢}{F}Fn{A}\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 rexrn.1 ${⊢}{x}={F}\left({y}\right)\to \left({\phi }↔{\psi }\right)$
2 fvexd ${⊢}\left({F}Fn{A}\wedge {y}\in {A}\right)\to {F}\left({y}\right)\in \mathrm{V}$
3 fvelrnb ${⊢}{F}Fn{A}\to \left({x}\in \mathrm{ran}{F}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)={x}\right)$
4 eqcom ${⊢}{F}\left({y}\right)={x}↔{x}={F}\left({y}\right)$
5 4 rexbii ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)={x}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}={F}\left({y}\right)$
6 3 5 syl6bb ${⊢}{F}Fn{A}\to \left({x}\in \mathrm{ran}{F}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}={F}\left({y}\right)\right)$
7 1 adantl ${⊢}\left({F}Fn{A}\wedge {x}={F}\left({y}\right)\right)\to \left({\phi }↔{\psi }\right)$
8 2 6 7 ralxfr2d ${⊢}{F}Fn{A}\to \left(\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$