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 y φ ψ
Assertion ralrn F Fn A x ran F φ y A ψ

Proof

Step Hyp Ref Expression
1 rexrn.1 x = F y φ ψ
2 fvexd F Fn A y A F y V
3 fvelrnb F Fn A x ran F y A F y = x
4 eqcom F y = x x = F y
5 4 rexbii y A F y = x y A x = F y
6 3 5 bitrdi F Fn A x ran F y A x = F y
7 1 adantl F Fn A x = F y φ ψ
8 2 6 7 ralxfr2d F Fn A x ran F φ y A ψ