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) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 ralima.x x = F y φ ψ
2 1 notbid x = F y ¬ φ ¬ ψ
3 2 ralima F Fn A B A x F B ¬ φ y B ¬ ψ
4 3 notbid F Fn A B A ¬ x F B ¬ φ ¬ y B ¬ ψ
5 dfrex2 x F B φ ¬ x F B ¬ φ
6 dfrex2 y B ψ ¬ y B ¬ ψ
7 4 5 6 3bitr4g F Fn A B A x F B φ y B ψ