Theorem bnj1383

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

	Ref	Expression
Hypotheses	bnj1383.1	|- ( ph <-> A. f e. A Fun f )
	bnj1383.2	|- D = ( dom f i^i dom g )
	bnj1383.3	|- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
Assertion	bnj1383	|- ( ps -> Fun U. A )

Proof

Step	Hyp	Ref	Expression
1		bnj1383.1	|- ( ph <-> A. f e. A Fun f )
2		bnj1383.2	|- D = ( dom f i^i dom g )
3		bnj1383.3	|- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
4		biid	|- ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) <-> ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) )
5		biid	|- ( ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) /\ f e. A /\ <. x , y >. e. f ) <-> ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) /\ f e. A /\ <. x , y >. e. f ) )
6		biid	|- ( ( ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) /\ f e. A /\ <. x , y >. e. f ) /\ g e. A /\ <. x , z >. e. g ) <-> ( ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) /\ f e. A /\ <. x , y >. e. f ) /\ g e. A /\ <. x , z >. e. g ) )
7	1 2 3 4 5 6	bnj1379	|- ( ps -> Fun U. A )