MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpt2ga Structured version   Visualization version   GIF version

Theorem ovmpt2ga 6936
Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
Hypotheses
Ref Expression
ovmpt2ga.1 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)
ovmpt2ga.2 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
Assertion
Ref Expression
ovmpt2ga ((𝐴𝐶𝐵𝐷𝑆𝐻) → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐻(𝑥,𝑦)

Proof of Theorem ovmpt2ga
StepHypRef Expression
1 elex 3361 . 2 (𝑆𝐻𝑆 ∈ V)
2 ovmpt2ga.2 . . . 4 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
32a1i 11 . . 3 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))
4 ovmpt2ga.1 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)
54adantl 467 . . 3 (((𝐴𝐶𝐵𝐷𝑆 ∈ V) ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)
6 simp1 1129 . . 3 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → 𝐴𝐶)
7 simp2 1130 . . 3 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → 𝐵𝐷)
8 simp3 1131 . . 3 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → 𝑆 ∈ V)
93, 5, 6, 7, 8ovmpt2d 6934 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
101, 9syl3an3 1168 1 ((𝐴𝐶𝐵𝐷𝑆𝐻) → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070   = wceq 1630  wcel 2144  Vcvv 3349  (class class class)co 6792  cmpt2 6794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797
This theorem is referenced by:  ovmpt2a  6937  ovmpt2g  6941  elovmpt2  7025  offval  7050  offval3  7308  mptmpt2opabbrd  7397  bropopvvv  7405  reps  13725  hashbcval  15912  setsvalg  16093  ressval  16133  restval  16294  sylow1lem4  18222  sylow3lem2  18249  sylow3lem3  18250  lsmvalx  18260  mvrfval  19634  opsrval  19688  marrepfval  20583  marrepval0  20584  marepvfval  20588  marepvval0  20589  cnmpt12  21690  cnmpt22  21697  qtopval  21718  flimval  21986  fclsval  22031  ucnval  22300  stdbdmetval  22538  resvval  30161  ofcfval3  30498  fmulcl  40325
  Copyright terms: Public domain W3C validator