![]() |
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 5695 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} | |
2 | nfxp.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2895 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfxp.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2895 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵 |
6 | 3, 5 | nfan 1897 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) |
7 | 6 | nfopab 5217 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} |
8 | 1, 7 | nfcxfr 2901 | 1 ⊢ Ⅎ𝑥(𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 ∈ wcel 2106 Ⅎwnfc 2888 {copab 5210 × cxp 5687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-opab 5211 df-xp 5695 |
This theorem is referenced by: opeliunxp 5756 nfres 6002 mpomptsx 8088 dmmpossx 8090 fmpox 8091 ovmptss 8117 nfdju 9945 axcc2 10475 fsum2dlem 15803 fsumcom2 15807 fprod2dlem 16013 fprodcom2 16017 gsumcom2 20008 prdsdsf 24393 prdsxmet 24395 djussxp2 32665 aciunf1lem 32679 gsumpart 33043 esum2dlem 34073 poimirlem16 37623 poimirlem19 37626 dvnprodlem1 45902 stoweidlem21 45977 stoweidlem47 46003 opeliun2xp 48178 dmmpossx2 48182 |
Copyright terms: Public domain | W3C validator |