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	|- ( ph -> Fun A )
	bnj1422.2	|- ( ph -> dom A = B )
Assertion	bnj1422	|- ( ph -> A Fn B )

Proof

Step	Hyp	Ref	Expression
1		bnj1422.1	|- ( ph -> Fun A )
2		bnj1422.2	|- ( ph -> dom A = B )
3		df-fn	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
4	1 2 3	sylanbrc	|- ( ph -> A Fn B )