Theorem bnj1386

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

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

Proof

Step	Hyp	Ref	Expression
1		bnj1386.1	|- ( ph <-> A. f e. A Fun f )
2		bnj1386.2	|- D = ( dom f i^i dom g )
3		bnj1386.3	|- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
4		bnj1386.4	|- ( x e. A -> A. f x e. A )
5		biid	|- ( A. h e. A Fun h <-> A. h e. A Fun h )
6		eqid	|- ( dom h i^i dom g ) = ( dom h i^i dom g )
7		biid	|- ( ( A. h e. A Fun h /\ A. h e. A A. g e. A ( h |` ( dom h i^i dom g ) ) = ( g |` ( dom h i^i dom g ) ) ) <-> ( A. h e. A Fun h /\ A. h e. A A. g e. A ( h |` ( dom h i^i dom g ) ) = ( g |` ( dom h i^i dom g ) ) ) )
8	1 2 3 4 5 6 7	bnj1385	|- ( ps -> Fun U. A )