Theorem bnj1422

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

	Ref	Expression
Hypotheses	bnj1422.1	⊢ ( 𝜑 → Fun 𝐴 )
	bnj1422.2	⊢ ( 𝜑 → dom 𝐴 = 𝐵 )
Assertion	bnj1422	⊢ ( 𝜑 → 𝐴 Fn 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bnj1422.1	⊢ ( 𝜑 → Fun 𝐴 )
2		bnj1422.2	⊢ ( 𝜑 → dom 𝐴 = 𝐵 )
3		df-fn	⊢ ( 𝐴 Fn 𝐵 ↔ ( Fun 𝐴 ∧ dom 𝐴 = 𝐵 ) )
4	1 2 3	sylanbrc	⊢ ( 𝜑 → 𝐴 Fn 𝐵 )