![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfmpo2 | 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 |
---|---|
nfmpo2 | ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpo 7435 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | nfoprab2 7494 | . 2 ⊢ Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | nfcxfr 2900 | 1 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1536 ∈ wcel 2105 Ⅎwnfc 2887 {coprab 7431 ∈ cmpo 7432 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-oprab 7434 df-mpo 7435 |
This theorem is referenced by: ovmpos 7580 ov2gf 7581 ovmpodxf 7582 ovmpodf 7588 ovmpodv2 7590 xpcomco 9100 mapxpen 9181 pwfseqlem2 10696 pwfseqlem4a 10698 pwfseqlem4 10699 gsum2d2lem 20005 gsum2d2 20006 gsumcom2 20007 dprd2d2 20078 cnmpt21 23694 cnmpt2t 23696 cnmptcom 23701 cnmpt2k 23711 xkocnv 23837 finxpreclem2 37372 finxpreclem6 37378 mnringmulrcld 44223 fmuldfeq 45538 smflimlem6 46731 ovmpordxf 48183 |
Copyright terms: Public domain | W3C validator |