Metamath Proof Explorer


Theorem bnj1386

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1386.1 φ f A Fun f
bnj1386.2 D = dom f dom g
bnj1386.3 ψ φ f A g A f D = g D
bnj1386.4 x A f x A
Assertion bnj1386 ψ Fun A

Proof

Step Hyp Ref Expression
1 bnj1386.1 φ f A Fun f
2 bnj1386.2 D = dom f dom g
3 bnj1386.3 ψ φ f A g A f D = g D
4 bnj1386.4 x A f x A
5 biid h A Fun h h A Fun h
6 eqid dom h dom g = dom h dom g
7 biid h A Fun h h A g A h dom h dom g = g dom h dom g h A Fun h h A g A h dom h dom g = g dom h dom g
8 1 2 3 4 5 6 7 bnj1385 ψ Fun A