| 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 20031 gsum2d2 20032 gsumcom2 20033 dprd2d2 20104 cnmpt21 23785 cnmpt2t 23787 cnmptcom 23792 cnmpt2k 23802 xkocnv 23928 finxpreclem2 37891 finxpreclem6 37897 mnringmulrcld 44811 fmuldfeq 46158 smflimlem6 47349 ovmpordxf 48971 |
| Copyright terms: Public domain | W3C validator |