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