![]() |
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 7357 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | nfoprab2 7414 | . 2 ⊢ Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | nfcxfr 2904 | 1 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∈ wcel 2107 Ⅎwnfc 2886 {coprab 7353 ∈ cmpo 7354 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-oprab 7356 df-mpo 7357 |
This theorem is referenced by: ovmpos 7498 ov2gf 7499 ovmpodxf 7500 ovmpodf 7506 ovmpodv2 7508 xpcomco 8965 mapxpen 9046 pwfseqlem2 10554 pwfseqlem4a 10556 pwfseqlem4 10557 gsum2d2lem 19709 gsum2d2 19710 gsumcom2 19711 dprd2d2 19782 cnmpt21 22974 cnmpt2t 22976 cnmptcom 22981 cnmpt2k 22991 xkocnv 23117 finxpreclem2 35793 finxpreclem6 35799 mnringmulrcld 42413 fmuldfeq 43719 smflimlem6 44912 ovmpordxf 46309 |
Copyright terms: Public domain | W3C validator |