# Metamath Proof Explorer

## 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 )