MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funfvbrb Structured version   Unicode version

Theorem funfvbrb 5835
Description: Two ways to say that  A is in the domain of  F. (Contributed by Mario Carneiro, 1-May-2014.)
Assertion
Ref Expression
funfvbrb  |-  ( Fun 
F  ->  ( A  e.  dom  F  <->  A F
( F `  A
) ) )

Proof of Theorem funfvbrb
StepHypRef Expression
1 funfvop 5834 . . 3  |-  ( ( Fun  F  /\  A  e.  dom  F )  ->  <. A ,  ( F `
 A ) >.  e.  F )
2 df-br 4205 . . 3  |-  ( A F ( F `  A )  <->  <. A , 
( F `  A
) >.  e.  F )
31, 2sylibr 204 . 2  |-  ( ( Fun  F  /\  A  e.  dom  F )  ->  A F ( F `  A ) )
4 funrel 5463 . . 3  |-  ( Fun 
F  ->  Rel  F )
5 releldm 5094 . . 3  |-  ( ( Rel  F  /\  A F ( F `  A ) )  ->  A  e.  dom  F )
64, 5sylan 458 . 2  |-  ( ( Fun  F  /\  A F ( F `  A ) )  ->  A  e.  dom  F )
73, 6impbida 806 1  |-  ( Fun 
F  ->  ( A  e.  dom  F  <->  A F
( F `  A
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1725   <.cop 3809   class class class wbr 4204   dom cdm 4870   Rel wrel 4875   Fun wfun 5440   ` cfv 5446
This theorem is referenced by:  fmptco  5893  fpwwe2lem13  8507  fpwwe2  8508  climdm  12338  invco  13986  funciso  14061  ffthiso  14116  fuciso  14162  setciso  14236  catciso  14252  lmcau  19255  dvcnp  19795  dvadd  19816  dvmul  19817  dvaddf  19818  dvmulf  19819  dvco  19823  dvcof  19824  dvcjbr  19825  dvcnvlem  19850  dvferm1  19859  dvferm2  19861  ulmdm  20299  ulmdvlem3  20308  minvecolem4a  22369  hlimf  22730  hhsscms  22769  occllem  22795  occl  22796  chscllem4  23132  fmptcof2  24066  heiborlem9  26482  bfplem1  26485
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-iota 5410  df-fun 5448  df-fn 5449  df-fv 5454
  Copyright terms: Public domain W3C validator