|   | 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 5690 | . 2 ⊢ (𝐴 × 𝐵) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} | |
| 2 | nfxp.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | nfcri 2896 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | 
| 4 | nfxp.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
| 5 | 4 | nfcri 2896 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵 | 
| 6 | 3, 5 | nfan 1898 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) | 
| 7 | 6 | nfopab 5211 | . 2 ⊢ Ⅎ𝑥{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} | 
| 8 | 1, 7 | nfcxfr 2902 | 1 ⊢ Ⅎ𝑥(𝐴 × 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∧ wa 395 ∈ wcel 2107 Ⅎwnfc 2889 {copab 5204 × cxp 5682 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-opab 5205 df-xp 5690 | 
| This theorem is referenced by: opeliunxp 5751 opeliun2xp 5752 nfres 5998 mpomptsx 8090 dmmpossx 8092 fmpox 8093 ovmptss 8119 nfdju 9948 axcc2 10478 fsum2dlem 15807 fsumcom2 15811 fprod2dlem 16017 fprodcom2 16021 gsumcom2 19994 prdsdsf 24378 prdsxmet 24380 iunxpssiun1 32582 djussxp2 32659 aciunf1lem 32673 gsumpart 33061 esum2dlem 34094 poimirlem16 37644 poimirlem19 37647 dvnprodlem1 45966 stoweidlem21 46041 stoweidlem47 46067 dmmpossx2 48258 | 
| Copyright terms: Public domain | W3C validator |