| 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 7405 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
| 2 | nfoprab2 7462 | . 2 ⊢ Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
| 3 | 1, 2 | nfcxfr 2925 | 1 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 400 = wceq 1563 ∈ wcel 2145 Ⅎwnfc 2912 {coprab 7401 ∈ cmpo 7402 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-ex 1803 df-nf 1807 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-oprab 7404 df-mpo 7405 |
| This theorem is referenced by: ovmpos 7548 ov2gf 7549 ovmpodxf 7550 ovmpodf 7556 ovmpodv2 7558 xpcomco 9043 mapxpen 9119 pwfseqlem2 10632 pwfseqlem4a 10634 pwfseqlem4 10635 gsum2d2lem 20034 gsum2d2 20035 gsumcom2 20036 dprd2d2 20107 cnmpt21 23789 cnmpt2t 23791 cnmptcom 23796 cnmpt2k 23806 xkocnv 23932 finxpreclem2 37896 finxpreclem6 37902 mnringmulrcld 44816 fmuldfeq 46157 smflimlem6 47348 ovmpordxf 48970 |
| Copyright terms: Public domain | W3C validator |