Theorem funfvbrb 6330

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

Step	Hyp	Ref	Expression
1		funfvop 6329	. . 3 |- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
2		df-br 4654	. . 3 |- ( A F ( F ` A ) <-> <. A , ( F ` A ) >. e. F )
3	1, 2	sylibr 224	. 2 |- ( ( Fun F /\ A e. dom F ) -> A F ( F ` A ) )
4		funrel 5905	. . 3 |- ( Fun F -> Rel F )
5		releldm 5358	. . 3 |- ( ( Rel F /\ A F ( F ` A ) ) -> A e. dom F )
6	4, 5	sylan 488	. 2 |- ( ( Fun F /\ A F ( F ` A ) ) -> A e. dom F )
7	3, 6	impbida 877	1 |- ( Fun F -> ( A e. dom F <-> A F ( F ` A ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   <.cop 4183   class class class wbr 4653   dom cdm 5114   Rel wrel 5119   Fun wfun 5882   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  fmptco  6396  fpwwe2lem13  9464  fpwwe2  9465  climdm  14285  invco  16431  funciso  16534  ffthiso  16589  fuciso  16635  setciso  16741  catciso  16757  lmcau  23111  dvcnp  23682  dvadd  23703  dvmul  23704  dvaddf  23705  dvmulf  23706  dvco  23710  dvcof  23711  dvcjbr  23712  dvcnvlem  23739  dvferm1  23748  dvferm2  23750  ulmdm  24147  ulmdvlem3  24156  minvecolem4a  27733  hlimf  28094  hhsscms  28136  occllem  28162  occl  28163  chscllem4  28499  fmptcof2  29457  heiborlem9  33618  bfplem1  33621  rngciso  41982  rngcisoALTV  41994  ringciso  42033  ringcisoALTV  42057