# Metamath Proof Explorer

## Theorem fmpox

Description: Functionality, domain and codomain of a class given by the maps-to notation, where B ( x ) is not constant but depends on x . (Contributed by NM, 29-Dec-2014)

Ref Expression
Hypothesis fmpox.1
`|- F = ( x e. A , y e. B |-> C )`
Assertion fmpox
`|- ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )`

### Proof

Step Hyp Ref Expression
1 fmpox.1
` |-  F = ( x e. A , y e. B |-> C )`
2 vex
` |-  z e. _V`
3 vex
` |-  w e. _V`
4 2 3 op1std
` |-  ( v = <. z , w >. -> ( 1st ` v ) = z )`
5 4 csbeq1d
` |-  ( v = <. z , w >. -> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C = [_ z / x ]_ [_ ( 2nd ` v ) / y ]_ C )`
6 2 3 op2ndd
` |-  ( v = <. z , w >. -> ( 2nd ` v ) = w )`
7 6 csbeq1d
` |-  ( v = <. z , w >. -> [_ ( 2nd ` v ) / y ]_ C = [_ w / y ]_ C )`
8 7 csbeq2dv
` |-  ( v = <. z , w >. -> [_ z / x ]_ [_ ( 2nd ` v ) / y ]_ C = [_ z / x ]_ [_ w / y ]_ C )`
9 5 8 eqtrd
` |-  ( v = <. z , w >. -> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C = [_ z / x ]_ [_ w / y ]_ C )`
10 9 eleq1d
` |-  ( v = <. z , w >. -> ( [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C e. D <-> [_ z / x ]_ [_ w / y ]_ C e. D ) )`
11 10 raliunxp
` |-  ( A. v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C e. D <-> A. z e. A A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D )`
12 nfv
` |-  F/ z ( ( x e. A /\ y e. B ) /\ v = C )`
13 nfv
` |-  F/ w ( ( x e. A /\ y e. B ) /\ v = C )`
14 nfv
` |-  F/ x z e. A`
15 nfcsb1v
` |-  F/_ x [_ z / x ]_ B`
16 15 nfcri
` |-  F/ x w e. [_ z / x ]_ B`
17 14 16 nfan
` |-  F/ x ( z e. A /\ w e. [_ z / x ]_ B )`
18 nfcsb1v
` |-  F/_ x [_ z / x ]_ [_ w / y ]_ C`
19 18 nfeq2
` |-  F/ x v = [_ z / x ]_ [_ w / y ]_ C`
20 17 19 nfan
` |-  F/ x ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C )`
21 nfv
` |-  F/ y ( z e. A /\ w e. [_ z / x ]_ B )`
22 nfcv
` |-  F/_ y z`
23 nfcsb1v
` |-  F/_ y [_ w / y ]_ C`
24 22 23 nfcsbw
` |-  F/_ y [_ z / x ]_ [_ w / y ]_ C`
25 24 nfeq2
` |-  F/ y v = [_ z / x ]_ [_ w / y ]_ C`
26 21 25 nfan
` |-  F/ y ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C )`
27 eleq1w
` |-  ( x = z -> ( x e. A <-> z e. A ) )`
` |-  ( ( x = z /\ y = w ) -> ( x e. A <-> z e. A ) )`
29 eleq1w
` |-  ( y = w -> ( y e. B <-> w e. B ) )`
30 csbeq1a
` |-  ( x = z -> B = [_ z / x ]_ B )`
31 30 eleq2d
` |-  ( x = z -> ( w e. B <-> w e. [_ z / x ]_ B ) )`
32 29 31 sylan9bbr
` |-  ( ( x = z /\ y = w ) -> ( y e. B <-> w e. [_ z / x ]_ B ) )`
33 28 32 anbi12d
` |-  ( ( x = z /\ y = w ) -> ( ( x e. A /\ y e. B ) <-> ( z e. A /\ w e. [_ z / x ]_ B ) ) )`
34 csbeq1a
` |-  ( y = w -> C = [_ w / y ]_ C )`
35 csbeq1a
` |-  ( x = z -> [_ w / y ]_ C = [_ z / x ]_ [_ w / y ]_ C )`
36 34 35 sylan9eqr
` |-  ( ( x = z /\ y = w ) -> C = [_ z / x ]_ [_ w / y ]_ C )`
37 36 eqeq2d
` |-  ( ( x = z /\ y = w ) -> ( v = C <-> v = [_ z / x ]_ [_ w / y ]_ C ) )`
38 33 37 anbi12d
` |-  ( ( x = z /\ y = w ) -> ( ( ( x e. A /\ y e. B ) /\ v = C ) <-> ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C ) ) )`
39 12 13 20 26 38 cbvoprab12
` |-  { <. <. x , y >. , v >. | ( ( x e. A /\ y e. B ) /\ v = C ) } = { <. <. z , w >. , v >. | ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C ) }`
40 df-mpo
` |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , v >. | ( ( x e. A /\ y e. B ) /\ v = C ) }`
41 df-mpo
` |-  ( z e. A , w e. [_ z / x ]_ B |-> [_ z / x ]_ [_ w / y ]_ C ) = { <. <. z , w >. , v >. | ( ( z e. A /\ w e. [_ z / x ]_ B ) /\ v = [_ z / x ]_ [_ w / y ]_ C ) }`
42 39 40 41 3eqtr4i
` |-  ( x e. A , y e. B |-> C ) = ( z e. A , w e. [_ z / x ]_ B |-> [_ z / x ]_ [_ w / y ]_ C )`
43 9 mpomptx
` |-  ( v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) |-> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C ) = ( z e. A , w e. [_ z / x ]_ B |-> [_ z / x ]_ [_ w / y ]_ C )`
44 42 1 43 3eqtr4i
` |-  F = ( v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) |-> [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C )`
45 44 fmpt
` |-  ( A. v e. U_ z e. A ( { z } X. [_ z / x ]_ B ) [_ ( 1st ` v ) / x ]_ [_ ( 2nd ` v ) / y ]_ C e. D <-> F : U_ z e. A ( { z } X. [_ z / x ]_ B ) --> D )`
46 11 45 bitr3i
` |-  ( A. z e. A A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D <-> F : U_ z e. A ( { z } X. [_ z / x ]_ B ) --> D )`
47 nfv
` |-  F/ z A. y e. B C e. D`
48 18 nfel1
` |-  F/ x [_ z / x ]_ [_ w / y ]_ C e. D`
49 15 48 nfralw
` |-  F/ x A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D`
50 nfv
` |-  F/ w C e. D`
51 23 nfel1
` |-  F/ y [_ w / y ]_ C e. D`
52 34 eleq1d
` |-  ( y = w -> ( C e. D <-> [_ w / y ]_ C e. D ) )`
53 50 51 52 cbvralw
` |-  ( A. y e. B C e. D <-> A. w e. B [_ w / y ]_ C e. D )`
54 35 eleq1d
` |-  ( x = z -> ( [_ w / y ]_ C e. D <-> [_ z / x ]_ [_ w / y ]_ C e. D ) )`
55 30 54 raleqbidv
` |-  ( x = z -> ( A. w e. B [_ w / y ]_ C e. D <-> A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D ) )`
56 53 55 syl5bb
` |-  ( x = z -> ( A. y e. B C e. D <-> A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D ) )`
57 47 49 56 cbvralw
` |-  ( A. x e. A A. y e. B C e. D <-> A. z e. A A. w e. [_ z / x ]_ B [_ z / x ]_ [_ w / y ]_ C e. D )`
58 nfcv
` |-  F/_ z ( { x } X. B )`
59 nfcv
` |-  F/_ x { z }`
60 59 15 nfxp
` |-  F/_ x ( { z } X. [_ z / x ]_ B )`
61 sneq
` |-  ( x = z -> { x } = { z } )`
62 61 30 xpeq12d
` |-  ( x = z -> ( { x } X. B ) = ( { z } X. [_ z / x ]_ B ) )`
63 58 60 62 cbviun
` |-  U_ x e. A ( { x } X. B ) = U_ z e. A ( { z } X. [_ z / x ]_ B )`
64 63 feq2i
` |-  ( F : U_ x e. A ( { x } X. B ) --> D <-> F : U_ z e. A ( { z } X. [_ z / x ]_ B ) --> D )`
65 46 57 64 3bitr4i
` |-  ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )`