![]() |
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 7414 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | nfoprab2 7471 | . 2 ⊢ Ⅎ𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | nfcxfr 2902 | 1 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∈ wcel 2107 Ⅎwnfc 2884 {coprab 7410 ∈ cmpo 7411 |
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 2704 |
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 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-oprab 7413 df-mpo 7414 |
This theorem is referenced by: ovmpos 7556 ov2gf 7557 ovmpodxf 7558 ovmpodf 7564 ovmpodv2 7566 xpcomco 9062 mapxpen 9143 pwfseqlem2 10654 pwfseqlem4a 10656 pwfseqlem4 10657 gsum2d2lem 19841 gsum2d2 19842 gsumcom2 19843 dprd2d2 19914 cnmpt21 23175 cnmpt2t 23177 cnmptcom 23182 cnmpt2k 23192 xkocnv 23318 finxpreclem2 36271 finxpreclem6 36277 mnringmulrcld 42987 fmuldfeq 44299 smflimlem6 45492 ovmpordxf 47014 |
Copyright terms: Public domain | W3C validator |