![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfxp | Structured version Visualization version GIF 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 5417 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} | |
2 | nfxp.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2928 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfxp.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2928 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵 |
6 | 3, 5 | nfan 1863 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) |
7 | 6 | nfopab 5002 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} |
8 | 1, 7 | nfcxfr 2932 | 1 ⊢ Ⅎ𝑥(𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 ∈ wcel 2051 Ⅎwnfc 2918 {copab 4996 × cxp 5409 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2752 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-opab 4997 df-xp 5417 |
This theorem is referenced by: opeliunxp 5473 nfres 5702 mpomptsx 7576 dmmpossx 7578 fmpox 7579 ovmptss 7602 nfdju 9136 axcc2 9663 fsum2dlem 14991 fsumcom2 14995 fprod2dlem 15200 fprodcom2 15204 gsumcom2 18860 prdsdsf 22695 prdsxmet 22697 aciunf1lem 30186 esum2dlem 31027 poimirlem16 34389 poimirlem19 34392 dvnprodlem1 41696 stoweidlem21 41772 stoweidlem47 41798 opeliun2xp 43780 dmmpossx2 43784 |
Copyright terms: Public domain | W3C validator |