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 7188 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | nfoprab1 7242 | . 2 ⊢ Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | nfcxfr 2898 | 1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1542 ∈ wcel 2114 Ⅎwnfc 2880 {coprab 7184 ∈ cmpo 7185 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-oprab 7187 df-mpo 7188 |
This theorem is referenced by: ovmpos 7326 ov2gf 7327 ovmpodxf 7328 ovmpodf 7334 ovmpodv2 7336 xpcomco 8669 mapxpen 8746 pwfseqlem2 10172 pwfseqlem4a 10174 pwfseqlem4 10175 gsum2d2lem 19225 gsum2d2 19226 gsumcom2 19227 dprd2d2 19298 cnmpt21 22435 cnmpt2t 22437 cnmptcom 22442 cnmpt2k 22452 xkocnv 22578 numclwlk2lem2f1o 28329 finxpreclem2 35217 mnringmulrcld 41429 fmuldfeqlem1 42706 fmuldfeq 42707 ovmpordxf 45256 |
Copyright terms: Public domain | W3C validator |