![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfxp | Structured version Visualization version Unicode version |
Description: Bound-variable hypothesis builder for Cartesian product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nfxp.1 |
![]() ![]() ![]() ![]() |
nfxp.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfxp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xp 4858 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfxp.1 |
. . . . 5
![]() ![]() ![]() ![]() | |
3 | 2 | nfcri 2596 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfxp.2 |
. . . . 5
![]() ![]() ![]() ![]() | |
5 | 4 | nfcri 2596 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | nfan 2021 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | nfopab 4481 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | nfcxfr 2600 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-opab 4475 df-xp 4858 |
This theorem is referenced by: opeliunxp 4904 nfres 5125 mpt2mptsx 6882 dmmpt2ssx 6884 fmpt2x 6885 ovmptss 6903 axcc2 8892 fsum2dlem 13879 fsumcom2 13883 fprod2dlem 14082 fprodcom2 14086 gsumcom2 17655 prdsdsf 21430 prdsxmet 21432 aciunf1lem 28312 esum2dlem 28961 poimirlem16 32000 poimirlem19 32003 dvnprodlem1 37858 stoweidlem21 37918 stoweidlem47 37945 opeliun2xp 40386 dmmpt2ssx2 40390 |
Copyright terms: Public domain | W3C validator |