Metamath Proof Explorer


Theorem oprabexd

Description: Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by AV, 9-Aug-2024)

Ref Expression
Hypotheses oprabexd.1 φ A V
oprabexd.2 φ B W
oprabexd.3 φ x A y B * z ψ
oprabexd.4 φ F = x y z | x A y B ψ
Assertion oprabexd φ F V

Proof

Step Hyp Ref Expression
1 oprabexd.1 φ A V
2 oprabexd.2 φ B W
3 oprabexd.3 φ x A y B * z ψ
4 oprabexd.4 φ F = x y z | x A y B ψ
5 3 ex φ x A y B * z ψ
6 moanimv * z x A y B ψ x A y B * z ψ
7 5 6 sylibr φ * z x A y B ψ
8 7 alrimivv φ x y * z x A y B ψ
9 funoprabg x y * z x A y B ψ Fun x y z | x A y B ψ
10 8 9 syl φ Fun x y z | x A y B ψ
11 dmoprabss dom x y z | x A y B ψ A × B
12 1 2 xpexd φ A × B V
13 ssexg dom x y z | x A y B ψ A × B A × B V dom x y z | x A y B ψ V
14 11 12 13 sylancr φ dom x y z | x A y B ψ V
15 funex Fun x y z | x A y B ψ dom x y z | x A y B ψ V x y z | x A y B ψ V
16 10 14 15 syl2anc φ x y z | x A y B ψ V
17 4 16 eqeltrd φ F V