Metamath Proof Explorer


Theorem imaeqsexvOLD

Description: Duplicate version of ralima . (Contributed by Scott Fenton, 27-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 imaeqsexvOLD.1 x = F y φ ψ
2 df-rex x F B φ x x F B φ
3 fvelimab F Fn A B A x F B y B F y = x
4 3 anbi1d F Fn A B A x F B φ y B F y = x φ
5 4 exbidv F Fn A B A x x F B φ x y B F y = x φ
6 2 5 bitrid F Fn A B A x F B φ x y B F y = x φ
7 rexcom4 y B x F y = x φ x y B F y = x φ
8 eqcom F y = x x = F y
9 8 anbi1i F y = x φ x = F y φ
10 9 exbii x F y = x φ x x = F y φ
11 fvex F y V
12 11 1 ceqsexv x x = F y φ ψ
13 10 12 bitri x F y = x φ ψ
14 13 rexbii y B x F y = x φ y B ψ
15 r19.41v y B F y = x φ y B F y = x φ
16 15 exbii x y B F y = x φ x y B F y = x φ
17 7 14 16 3bitr3ri x y B F y = x φ y B ψ
18 6 17 bitrdi F Fn A B A x F B φ y B ψ