Metamath Proof Explorer


Theorem fnoprabg

Description: Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007)

Ref Expression
Assertion fnoprabg x y φ ∃! z ψ x y z | φ ψ Fn x y | φ

Proof

Step Hyp Ref Expression
1 eumo ∃! z ψ * z ψ
2 1 imim2i φ ∃! z ψ φ * z ψ
3 moanimv * z φ ψ φ * z ψ
4 2 3 sylibr φ ∃! z ψ * z φ ψ
5 4 2alimi x y φ ∃! z ψ x y * z φ ψ
6 funoprabg x y * z φ ψ Fun x y z | φ ψ
7 5 6 syl x y φ ∃! z ψ Fun x y z | φ ψ
8 dmoprab dom x y z | φ ψ = x y | z φ ψ
9 nfa1 x x y φ ∃! z ψ
10 nfa2 y x y φ ∃! z ψ
11 simpl φ ψ φ
12 11 exlimiv z φ ψ φ
13 euex ∃! z ψ z ψ
14 13 imim2i φ ∃! z ψ φ z ψ
15 14 ancld φ ∃! z ψ φ φ z ψ
16 19.42v z φ ψ φ z ψ
17 15 16 syl6ibr φ ∃! z ψ φ z φ ψ
18 12 17 impbid2 φ ∃! z ψ z φ ψ φ
19 18 sps y φ ∃! z ψ z φ ψ φ
20 19 sps x y φ ∃! z ψ z φ ψ φ
21 9 10 20 opabbid x y φ ∃! z ψ x y | z φ ψ = x y | φ
22 8 21 eqtrid x y φ ∃! z ψ dom x y z | φ ψ = x y | φ
23 df-fn x y z | φ ψ Fn x y | φ Fun x y z | φ ψ dom x y z | φ ψ = x y | φ
24 7 22 23 sylanbrc x y φ ∃! z ψ x y z | φ ψ Fn x y | φ