Metamath Proof Explorer


Theorem ralima

Description: Universal 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 ralima F Fn A B A x F B φ y B ψ

Proof

Step Hyp Ref Expression
1 ralima.x x = F y φ ψ
2 fnfun F Fn A Fun F
3 2 funfnd F Fn A F Fn dom F
4 fndm F Fn A dom F = A
5 4 sseq2d F Fn A B dom F B A
6 5 biimpar F Fn A B A B dom F
7 fvexd F Fn dom F B dom F y B F y V
8 fvelimab F Fn dom F B dom F x F B y B F y = x
9 eqcom F y = x x = F y
10 9 rexbii y B F y = x y B x = F y
11 8 10 bitrdi F Fn dom F B dom F x F B y B x = F y
12 1 adantl F Fn dom F B dom F x = F y φ ψ
13 7 11 12 ralxfr2d F Fn dom F B dom F x F B φ y B ψ
14 3 6 13 syl2an2r F Fn A B A x F B φ y B ψ