Metamath Proof Explorer


Theorem rexima

Description: Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Hypothesis rexima.x x = F y φ ψ
Assertion rexima F Fn A B A x F B φ y B ψ

Proof

Step Hyp Ref Expression
1 rexima.x x = F y φ ψ
2 fvexd F Fn A B A y B F y V
3 fvelimab F Fn A B A x F B y B F y = x
4 eqcom F y = x x = F y
5 4 rexbii y B F y = x y B x = F y
6 3 5 bitrdi F Fn A B A x F B y B x = F y
7 1 adantl F Fn A B A x = F y φ ψ
8 2 6 7 rexxfr2d F Fn A B A x F B φ y B ψ