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

Theorem funbrfv 6027
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 5706 . . . 4 (Fun 𝐹 → Rel 𝐹)
2 brrelex2 4975 . . . 4 ((Rel 𝐹𝐴𝐹𝐵) → 𝐵 ∈ V)
31, 2sylan 486 . . 3 ((Fun 𝐹𝐴𝐹𝐵) → 𝐵 ∈ V)
4 breq2 4485 . . . . . 6 (𝑦 = 𝐵 → (𝐴𝐹𝑦𝐴𝐹𝐵))
54anbi2d 735 . . . . 5 (𝑦 = 𝐵 → ((Fun 𝐹𝐴𝐹𝑦) ↔ (Fun 𝐹𝐴𝐹𝐵)))
6 eqeq2 2525 . . . . 5 (𝑦 = 𝐵 → ((𝐹𝐴) = 𝑦 ↔ (𝐹𝐴) = 𝐵))
75, 6imbi12d 332 . . . 4 (𝑦 = 𝐵 → (((Fun 𝐹𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦) ↔ ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵)))
8 funeu 5713 . . . . . 6 ((Fun 𝐹𝐴𝐹𝑦) → ∃!𝑦 𝐴𝐹𝑦)
9 tz6.12-1 6003 . . . . . 6 ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
108, 9sylan2 489 . . . . 5 ((𝐴𝐹𝑦 ∧ (Fun 𝐹𝐴𝐹𝑦)) → (𝐹𝐴) = 𝑦)
1110anabss7 857 . . . 4 ((Fun 𝐹𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
127, 11vtoclg 3143 . . 3 (𝐵 ∈ V → ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵))
133, 12mpcom 37 . 2 ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵)
1413ex 448 1 (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹𝐴) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1938  ∃!weu 2362  Vcvv 3077   class class class wbr 4481  Rel wrel 4937  Fun wfun 5683  cfv 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-iota 5653  df-fun 5691  df-fv 5697
This theorem is referenced by:  funopfv  6028  fnbrfvb  6029  fvelima  6041  fvi  6048  opabiota  6054  fmptco  6186  fliftfun  6338  fliftval  6342  tfrlem5  7238  fpwwe2  9219  nqerid  9509  sum0  14166  sumz  14167  fsumsers  14173  isumclim  14197  ntrivcvgfvn0  14337  ntrivcvgtail  14338  zprodn0  14375  iprodclim  14435  idinv  16162  cnextfvval  21580  cnextfres  21584  dvadd  23385  dvmul  23386  dvco  23392  dvcj  23395  dvrec  23400  dvcnv  23420  dvef  23423  ftc1cn  23486  ulmdv  23849  minvecolem4b  26897  minvecolem4  26899  minvecolem4bOLD  26907  minvecolem4OLD  26909  hlimuni  27268  chscllem4  27672  fmptcof2  28628  fvtransport  31145  fvray  31254  fvline  31257  ftc1cnnc  32529  frege124d  36954
  Copyright terms: Public domain W3C validator