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

Theorem funbrfv 5968
Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
funbrfv (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹𝐴) = 𝐵))

Proof of Theorem funbrfv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 funrel 5650 . . . 4 (Fun 𝐹 → Rel 𝐹)
2 brrelex2 4921 . . . 4 ((Rel 𝐹𝐴𝐹𝐵) → 𝐵 ∈ V)
31, 2sylan 481 . . 3 ((Fun 𝐹𝐴𝐹𝐵) → 𝐵 ∈ V)
4 breq2 4438 . . . . . 6 (𝑦 = 𝐵 → (𝐴𝐹𝑦𝐴𝐹𝐵))
54anbi2d 727 . . . . 5 (𝑦 = 𝐵 → ((Fun 𝐹𝐴𝐹𝑦) ↔ (Fun 𝐹𝐴𝐹𝐵)))
6 eqeq2 2516 . . . . 5 (𝑦 = 𝐵 → ((𝐹𝐴) = 𝑦 ↔ (𝐹𝐴) = 𝐵))
75, 6imbi12d 329 . . . 4 (𝑦 = 𝐵 → (((Fun 𝐹𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦) ↔ ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵)))
8 funeu 5657 . . . . . 6 ((Fun 𝐹𝐴𝐹𝑦) → ∃!𝑦 𝐴𝐹𝑦)
9 tz6.12-1 5944 . . . . . 6 ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
108, 9sylan2 484 . . . . 5 ((𝐴𝐹𝑦 ∧ (Fun 𝐹𝐴𝐹𝑦)) → (𝐹𝐴) = 𝑦)
1110anabss7 848 . . . 4 ((Fun 𝐹𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
127, 11vtoclg 3128 . . 3 (𝐵 ∈ V → ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵))
133, 12mpcom 37 . 2 ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵)
1413ex 443 1 (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378   = wceq 1468  wcel 1937  ∃!weu 2353  Vcvv 3066   class class class wbr 4434  Rel wrel 4885  Fun wfun 5627  cfv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-id 4795  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-iota 5597  df-fun 5635  df-fv 5641
This theorem is referenced by:  funopfv  5969  fnbrfvb  5970  fvelima  5982  fvi  5989  opabiota  5995  fmptco  6124  fliftfun  6276  fliftval  6280  tfrlem5  7175  fpwwe2  9153  nqerid  9443  sum0  13947  sumz  13948  fsumsers  13954  isumclim  13978  ntrivcvgfvn0  14115  ntrivcvgtail  14116  zprodn0  14153  iprodclim  14211  idinv  15860  cnextfvval  21238  cnextfres  21242  dvadd  23055  dvmul  23056  dvco  23062  dvcj  23065  dvrec  23070  dvcnv  23090  dvef  23093  ftc1cn  23156  ulmdv  23519  minvecolem4b  26683  minvecolem4  26685  minvecolem4bOLD  26693  minvecolem4OLD  26695  hlimuni  27054  chscllem4  27456  fmptcof2  28416  fvtransport  30950  fvray  31059  fvline  31062  ftc1cnnc  32254  frege124d  36592
  Copyright terms: Public domain W3C validator