![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-mpt2 | GIF version |
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, y (in A × B) to B(x, y)." An extension of df-mpt 3811 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Ref | Expression |
---|---|
df-mpt2 | ⊢ (x ∈ A, y ∈ B ↦ 𝐶) = {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar x | |
2 | vy | . . 3 setvar y | |
3 | cA | . . 3 class A | |
4 | cB | . . 3 class B | |
5 | cC | . . 3 class 𝐶 | |
6 | 1, 2, 3, 4, 5 | cmpt2 5457 | . 2 class (x ∈ A, y ∈ B ↦ 𝐶) |
7 | 1 | cv 1241 | . . . . . 6 class x |
8 | 7, 3 | wcel 1390 | . . . . 5 wff x ∈ A |
9 | 2 | cv 1241 | . . . . . 6 class y |
10 | 9, 4 | wcel 1390 | . . . . 5 wff y ∈ B |
11 | 8, 10 | wa 97 | . . . 4 wff (x ∈ A ∧ y ∈ B) |
12 | vz | . . . . . 6 setvar z | |
13 | 12 | cv 1241 | . . . . 5 class z |
14 | 13, 5 | wceq 1242 | . . . 4 wff z = 𝐶 |
15 | 11, 14 | wa 97 | . . 3 wff ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶) |
16 | 15, 1, 2, 12 | coprab 5456 | . 2 class {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)} |
17 | 6, 16 | wceq 1242 | 1 wff (x ∈ A, y ∈ B ↦ 𝐶) = {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)} |
Colors of variables: wff set class |
This definition is referenced by: mpt2eq123 5506 mpt2eq123dva 5508 mpt2eq3dva 5511 nfmpt21 5513 nfmpt22 5514 nfmpt2 5515 mpt20 5516 cbvmpt2x 5524 mpt2v 5536 mpt2mptx 5537 resmpt2 5541 mpt2fun 5545 mpt22eqb 5552 rnmpt2 5553 reldmmpt2 5554 ovmpt4g 5565 elmpt2cl 5640 fmpt2x 5768 tposmpt2 5837 erovlem 6134 xpcomco 6236 dfplpq2 6338 dfmpq2 6339 |
Copyright terms: Public domain | W3C validator |