Theorem bnj519

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

	Ref	Expression
Hypothesis	bnj519.1	|- A e. _V
Assertion	bnj519	|- ( B e. _V -> Fun { <. A , B >. } )

Proof

Step	Hyp	Ref	Expression
1		bnj519.1	|- A e. _V
2		funsng	|- ( ( A e. _V /\ B e. _V ) -> Fun { <. A , B >. } )
3	1 2	mpan	|- ( B e. _V -> Fun { <. A , B >. } )