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

Theorem funbrfv 6387
 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 6058 . . . 4 (Fun 𝐹 → Rel 𝐹)
2 brrelex2 5306 . . . 4 ((Rel 𝐹𝐴𝐹𝐵) → 𝐵 ∈ V)
31, 2sylan 489 . . 3 ((Fun 𝐹𝐴𝐹𝐵) → 𝐵 ∈ V)
4 breq2 4800 . . . . . 6 (𝑦 = 𝐵 → (𝐴𝐹𝑦𝐴𝐹𝐵))
54anbi2d 742 . . . . 5 (𝑦 = 𝐵 → ((Fun 𝐹𝐴𝐹𝑦) ↔ (Fun 𝐹𝐴𝐹𝐵)))
6 eqeq2 2763 . . . . 5 (𝑦 = 𝐵 → ((𝐹𝐴) = 𝑦 ↔ (𝐹𝐴) = 𝐵))
75, 6imbi12d 333 . . . 4 (𝑦 = 𝐵 → (((Fun 𝐹𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦) ↔ ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵)))
8 funeu 6066 . . . . . 6 ((Fun 𝐹𝐴𝐹𝑦) → ∃!𝑦 𝐴𝐹𝑦)
9 tz6.12-1 6363 . . . . . 6 ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
108, 9sylan2 492 . . . . 5 ((𝐴𝐹𝑦 ∧ (Fun 𝐹𝐴𝐹𝑦)) → (𝐹𝐴) = 𝑦)
1110anabss7 897 . . . 4 ((Fun 𝐹𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
127, 11vtoclg 3398 . . 3 (𝐵 ∈ V → ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵))
133, 12mpcom 38 . 2 ((Fun 𝐹𝐴𝐹𝐵) → (𝐹𝐴) = 𝐵)
1413ex 449 1 (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹𝐴) = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624   ∈ wcel 2131  ∃!weu 2599  Vcvv 3332   class class class wbr 4796  Rel wrel 5263  Fun wfun 6035  ‘cfv 6041 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-iota 6004  df-fun 6043  df-fv 6049 This theorem is referenced by:  funopfv  6388  fnbrfvb  6389  fvelima  6402  fvi  6409  opabiota  6415  fmptco  6551  fliftfun  6717  fliftval  6721  tfrlem5  7637  fpwwe2  9649  nqerid  9939  sum0  14643  sumz  14644  fsumsers  14650  isumclim  14679  ntrivcvgfvn0  14822  ntrivcvgtail  14823  zprodn0  14860  iprodclim  14920  idinv  16642  cnextfvval  22062  cnextfres  22066  dvadd  23894  dvmul  23895  dvco  23901  dvcj  23904  dvrec  23909  dvcnv  23931  dvef  23934  ftc1cn  23997  ulmdv  24348  minvecolem4b  28035  minvecolem4  28037  hlimuni  28396  chscllem4  28800  fmptcof2  29758  fvtransport  32437  fvray  32546  fvline  32549  ftc1cnnc  33789  frege124d  38547  fvelimad  39949  fvelima2  39966
 Copyright terms: Public domain W3C validator