Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfmpt22 | Structured version Visualization version Unicode version |
Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
Ref | Expression |
---|---|
nfmpt22 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt2 6655 | . 2 | |
2 | nfoprab2 6705 | . 2 | |
3 | 1, 2 | nfcxfr 2762 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 384 wceq 1483 wcel 1990 wnfc 2751 coprab 6651 cmpt2 6652 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-oprab 6654 df-mpt2 6655 |
This theorem is referenced by: ovmpt2s 6784 ov2gf 6785 ovmpt2dxf 6786 ovmpt2df 6792 ovmpt2dv2 6794 xpcomco 8050 mapxpen 8126 pwfseqlem2 9481 pwfseqlem4a 9483 pwfseqlem4 9484 gsum2d2lem 18372 gsum2d2 18373 gsumcom2 18374 dprd2d2 18443 cnmpt21 21474 cnmpt2t 21476 cnmptcom 21481 cnmpt2k 21491 xkocnv 21617 finxpreclem2 33227 finxpreclem6 33233 fmuldfeq 39815 smflimlem6 40984 ovmpt2rdxf 42117 |
Copyright terms: Public domain | W3C validator |