![]() |
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 7436 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | nfoprab1 7494 | . 2 ⊢ Ⅎ𝑥{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | nfcxfr 2901 | 1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1537 ∈ wcel 2106 Ⅎwnfc 2888 {coprab 7432 ∈ cmpo 7433 |
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-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-oprab 7435 df-mpo 7436 |
This theorem is referenced by: ovmpos 7581 ov2gf 7582 ovmpodxf 7583 ovmpodf 7589 ovmpodv2 7591 xpcomco 9101 mapxpen 9182 pwfseqlem2 10697 pwfseqlem4a 10699 pwfseqlem4 10700 gsum2d2lem 20006 gsum2d2 20007 gsumcom2 20008 dprd2d2 20079 cnmpt21 23695 cnmpt2t 23697 cnmptcom 23702 cnmpt2k 23712 xkocnv 23838 numclwlk2lem2f1o 30408 finxpreclem2 37373 mnringmulrcld 44224 fmuldfeqlem1 45538 fmuldfeq 45539 ovmpordxf 48184 |
Copyright terms: Public domain | W3C validator |