Theorem ovmpt4g 7515

Description: Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 6961.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)

Hypothesis

Ref	Expression
ovmpt4g.3	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Assertion

Ref	Expression
ovmpt4g	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem ovmpt4g

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elisset 2819	. . 3 ⊢ (𝐶 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐶)
2		moeq 3667	. . . . . . 7 ⊢ ∃*𝑧 𝑧 = 𝐶
3	2	a1i 11	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧 𝑧 = 𝐶)
4		ovmpt4g.3	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5		df-mpo 7373	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	4, 5	eqtri 2760	. . . . . 6 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7	3, 6	ovidi 7511	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝑧))
8		eqeq2 2749	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑥𝐹𝑦) = 𝑧 ↔ (𝑥𝐹𝑦) = 𝐶))
9	7, 8	mpbidi 241	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝐶))
10	9	exlimdv 1935	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑧 𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝐶))
11	1, 10	syl5 34	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐶 ∈ 𝑉 → (𝑥𝐹𝑦) = 𝐶))
12	11	3impia 1118	1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃*wmo 2538  (class class class)co 7368  {coprab 7369   ∈ cmpo 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  ovmpos  7516  ov2gf  7517  ovmpodxf  7518  ovmpodf  7524  ofmres  7938  fnmpoovd  8039  mapxpen  9083  pwfseqlem2  10582  pwfseqlem3  10583  fullfunc  17844  fthfunc  17845  prfcl  18138  curf1cl  18163  curfcl  18167  hofcl  18194  gsum2d2lem  19914  gsum2d2  19915  gsumcom2  19916  dprdval  19946  dprd2d2  19987  cnmpt21  23627  cnmpt2t  23629  cnmptcom  23634  cnmpt2k  23644  xkocnv  23770  suppovss  32771  fedgmullem1  33807  fedgmullem2  33808  fedgmul  33809  madjusmdetlem1  34005  madjusmdetlem3  34007  finxpreclem5  37650  sdclem2  37993  smflimlem1  47129  smflimlem2  47130  aovmpt4g  47561  ovmpordxf  48699  ovmpt4d  49224  iinfconstbas  49425  rescofuf  49452