Metamath Proof Explorer


Theorem mpofunOLD

Description: Obsolete version of mpofun as of 23-Jul-2024. (Contributed by Scott Fenton, 21-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis mpofun.1
|- F = ( x e. A , y e. B |-> C )
Assertion mpofunOLD
|- Fun F

Proof

Step Hyp Ref Expression
1 mpofun.1
 |-  F = ( x e. A , y e. B |-> C )
2 eqtr3
 |-  ( ( z = C /\ w = C ) -> z = w )
3 2 ad2ant2l
 |-  ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w )
4 3 gen2
 |-  A. z A. w ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w )
5 eqeq1
 |-  ( z = w -> ( z = C <-> w = C ) )
6 5 anbi2d
 |-  ( z = w -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ w = C ) ) )
7 6 mo4
 |-  ( E* z ( ( x e. A /\ y e. B ) /\ z = C ) <-> A. z A. w ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w ) )
8 4 7 mpbir
 |-  E* z ( ( x e. A /\ y e. B ) /\ z = C )
9 8 funoprab
 |-  Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
10 df-mpo
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
11 1 10 eqtri
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
12 11 funeqi
 |-  ( Fun F <-> Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } )
13 9 12 mpbir
 |-  Fun F