|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nfmpo1 | Structured version Visualization version GIF version | ||
| Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) | 
| Ref | Expression | 
|---|---|
| nfmpo1 | ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-mpo 7437 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
| 2 | nfoprab1 7495 | . 2 ⊢ Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
| 3 | 1, 2 | nfcxfr 2902 | 1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∧ wa 395 = wceq 1539 ∈ wcel 2107 Ⅎwnfc 2889 {coprab 7433 ∈ cmpo 7434 | 
| 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-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-oprab 7436 df-mpo 7437 | 
| This theorem is referenced by: ovmpos 7582 ov2gf 7583 ovmpodxf 7584 ovmpodf 7590 ovmpodv2 7592 xpcomco 9103 mapxpen 9184 pwfseqlem2 10700 pwfseqlem4a 10702 pwfseqlem4 10703 gsum2d2lem 19992 gsum2d2 19993 gsumcom2 19994 dprd2d2 20065 cnmpt21 23680 cnmpt2t 23682 cnmptcom 23687 cnmpt2k 23697 xkocnv 23823 numclwlk2lem2f1o 30399 finxpreclem2 37392 mnringmulrcld 44252 fmuldfeqlem1 45602 fmuldfeq 45603 ovmpordxf 48260 | 
| Copyright terms: Public domain | W3C validator |