Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfmpo.1 | |- F/_ z A |
|
nfmpo.2 | |- F/_ z B |
||
nfmpo.3 | |- F/_ z C |
||
Assertion | nfmpo | |- F/_ z ( x e. A , y e. B |-> C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfmpo.1 | |- F/_ z A |
|
2 | nfmpo.2 | |- F/_ z B |
|
3 | nfmpo.3 | |- F/_ z C |
|
4 | df-mpo | |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = C ) } |
|
5 | 1 | nfcri | |- F/ z x e. A |
6 | 2 | nfcri | |- F/ z y e. B |
7 | 5 6 | nfan | |- F/ z ( x e. A /\ y e. B ) |
8 | 3 | nfeq2 | |- F/ z w = C |
9 | 7 8 | nfan | |- F/ z ( ( x e. A /\ y e. B ) /\ w = C ) |
10 | 9 | nfoprab | |- F/_ z { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = C ) } |
11 | 4 10 | nfcxfr | |- F/_ z ( x e. A , y e. B |-> C ) |