![]() |
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 5681 | . 2 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} | |
2 | nfxp.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2890 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfxp.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2890 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵 |
6 | 3, 5 | nfan 1902 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) |
7 | 6 | nfopab 5216 | . 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} |
8 | 1, 7 | nfcxfr 2901 | 1 ⊢ Ⅎ𝑥(𝐴 × 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 ∈ wcel 2106 Ⅎwnfc 2883 {copab 5209 × cxp 5673 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-opab 5210 df-xp 5681 |
This theorem is referenced by: opeliunxp 5741 nfres 5981 mpomptsx 8046 dmmpossx 8048 fmpox 8049 ovmptss 8075 nfdju 9898 axcc2 10428 fsum2dlem 15712 fsumcom2 15716 fprod2dlem 15920 fprodcom2 15924 gsumcom2 19837 prdsdsf 23864 prdsxmet 23866 djussxp2 31860 aciunf1lem 31874 gsumpart 32194 esum2dlem 33078 poimirlem16 36492 poimirlem19 36495 dvnprodlem1 44648 stoweidlem21 44723 stoweidlem47 44749 opeliun2xp 46961 dmmpossx2 46965 |
Copyright terms: Public domain | W3C validator |