ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpov GIF version

Theorem mpov 5932
Description: Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
Assertion
Ref Expression
mpov (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶}
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝑧,𝐶
Allowed substitution hints:   𝐶(𝑥,𝑦)

Proof of Theorem mpov
StepHypRef Expression
1 df-mpo 5847 . 2 (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ V ∧ 𝑦 ∈ V) ∧ 𝑧 = 𝐶)}
2 vex 2729 . . . . 5 𝑥 ∈ V
3 vex 2729 . . . . 5 𝑦 ∈ V
42, 3pm3.2i 270 . . . 4 (𝑥 ∈ V ∧ 𝑦 ∈ V)
54biantrur 301 . . 3 (𝑧 = 𝐶 ↔ ((𝑥 ∈ V ∧ 𝑦 ∈ V) ∧ 𝑧 = 𝐶))
65oprabbii 5897 . 2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ V ∧ 𝑦 ∈ V) ∧ 𝑧 = 𝐶)}
71, 6eqtr4i 2189 1 (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶}
Colors of variables: wff set class
Syntax hints:  wa 103   = wceq 1343  wcel 2136  Vcvv 2726  {coprab 5843  cmpo 5844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728  df-oprab 5846  df-mpo 5847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator