This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )