Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfmpt22 | 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 |
---|---|
nfmpt22 | ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt2 6554 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | nfoprab2 6603 | . 2 ⊢ Ⅎ𝑦{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | nfcxfr 2749 | 1 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1475 ∈ wcel 1977 Ⅎwnfc 2738 {coprab 6550 ↦ cmpt2 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-oprab 6553 df-mpt2 6554 |
This theorem is referenced by: ovmpt2s 6682 ov2gf 6683 ovmpt2dxf 6684 ovmpt2df 6690 ovmpt2dv2 6692 xpcomco 7935 mapxpen 8011 pwfseqlem2 9360 pwfseqlem4a 9362 pwfseqlem4 9363 gsum2d2lem 18195 gsum2d2 18196 gsumcom2 18197 dprd2d2 18266 cnmpt21 21284 cnmpt2t 21286 cnmptcom 21291 cnmpt2k 21301 xkocnv 21427 finxpreclem2 32403 finxpreclem6 32409 fmuldfeq 38650 smflimlem6 39662 ovmpt2rdxf 41910 |
Copyright terms: Public domain | W3C validator |