Metamath Proof Explorer


Theorem bnj1502

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

Ref Expression
Hypotheses bnj1502.1 ( 𝜑 → Fun 𝐹 )
bnj1502.2 ( 𝜑𝐺𝐹 )
bnj1502.3 ( 𝜑𝐴 ∈ dom 𝐺 )
Assertion bnj1502 ( 𝜑 → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )

Proof

Step Hyp Ref Expression
1 bnj1502.1 ( 𝜑 → Fun 𝐹 )
2 bnj1502.2 ( 𝜑𝐺𝐹 )
3 bnj1502.3 ( 𝜑𝐴 ∈ dom 𝐺 )
4 funssfv ( ( Fun 𝐹𝐺𝐹𝐴 ∈ dom 𝐺 ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )
5 1 2 3 4 syl3anc ( 𝜑 → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )