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

Theorem funbrfvb 6396
Description: Equivalence of function value and binary relation. (Contributed by NM, 26-Mar-2006.)
Assertion
Ref Expression
funbrfvb ((Fun 𝐹𝐴 ∈ dom 𝐹) → ((𝐹𝐴) = 𝐵𝐴𝐹𝐵))

Proof of Theorem funbrfvb
StepHypRef Expression
1 funfn 6072 . 2 (Fun 𝐹𝐹 Fn dom 𝐹)
2 fnbrfvb 6394 . 2 ((𝐹 Fn dom 𝐹𝐴 ∈ dom 𝐹) → ((𝐹𝐴) = 𝐵𝐴𝐹𝐵))
31, 2sylanb 571 1 ((Fun 𝐹𝐴 ∈ dom 𝐹) → ((𝐹𝐴) = 𝐵𝐴𝐹𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383   = wceq 1634  wcel 2148   class class class wbr 4797  dom cdm 5263  Fun wfun 6036   Fn wfn 6037  cfv 6042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-iota 6005  df-fun 6044  df-fn 6045  df-fv 6050
This theorem is referenced by:  funbrfv2b  6399  dfimafn  6404  funimass4  6406  dcomex  9492  dvidlem  23920  taylthlem1  24368  dfimafnf  29793  funcnvmptOLD  29824  funcnvmpt  29825  eqfunresadj  32014  frege124d  38593  frege129d  38595  ntrclsfv1  38893  ntrneifv1  38917  ntrneifv2  38918
  Copyright terms: Public domain W3C validator